Skip to content

Commit 2ef8499

Browse files
committed
constify symex_bmct::record_coverage
This member is never written to and serves merely as a cache for a front-end option, so this commit makes it const.
1 parent 698aebd commit 2ef8499

File tree

3 files changed

+2
-6
lines changed

3 files changed

+2
-6
lines changed

src/cbmc/bmc.h

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,6 @@ class bmct:public safety_checkert
8686
ui_message_handler(_message_handler),
8787
driver_callback_after_symex(callback_after_symex)
8888
{
89-
symex.record_coverage=
90-
!options.get_option("symex-coverage-report").empty();
9189
}
9290

9391
virtual resultt run(const goto_functionst &goto_functions)
@@ -159,8 +157,6 @@ class bmct:public safety_checkert
159157
ui_message_handler(_message_handler),
160158
driver_callback_after_symex(callback_after_symex)
161159
{
162-
symex.record_coverage =
163-
!options.get_option("symex-coverage-report").empty();
164160
INVARIANT(
165161
options.get_bool_option("paths"),
166162
"Should only use saved equation & goto_state constructor "

src/cbmc/symex_bmc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ symex_bmct::symex_bmct(
2525
const optionst &options,
2626
path_storaget &path_storage)
2727
: goto_symext(mh, outer_symbol_table, _target, options, path_storage),
28-
record_coverage(false),
28+
record_coverage(!options.get_option("symex-coverage-report").empty()),
2929
symex_coverage(ns)
3030
{
3131
}

src/cbmc/symex_bmc.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ class symex_bmct: public goto_symext
8080
return symex_coverage.generate_report(goto_functions, path);
8181
}
8282

83-
bool record_coverage;
83+
const bool record_coverage;
8484

8585
unwindsett unwindset;
8686

0 commit comments

Comments
 (0)