Skip to content

Commit 5f77d95

Browse files
committed
const and protect self_loops_to_assumptions
This goto_symext member is never written to and serves merely as a cache for a front-end option, so this commit makes it const and protected.
1 parent 673ac81 commit 5f77d95

File tree

2 files changed

+3
-5
lines changed

2 files changed

+3
-5
lines changed

src/cbmc/bmc.h

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,8 +88,6 @@ class bmct:public safety_checkert
8888
{
8989
symex.record_coverage=
9090
!options.get_option("symex-coverage-report").empty();
91-
symex.self_loops_to_assumptions =
92-
options.get_bool_option("self-loops-to-assumptions");
9391
}
9492

9593
virtual resultt run(const goto_functionst &goto_functions)

src/goto-symex/goto_symex.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,9 +62,10 @@ class goto_symext
6262
options.get_bool_option("allow-pointer-unsoundness")),
6363
total_vccs(0),
6464
remaining_vccs(0),
65-
self_loops_to_assumptions(true),
6665
language_mode(),
6766
constant_propagation(options.get_bool_option("propagation")),
67+
self_loops_to_assumptions(
68+
options.get_bool_option("self-loops-to-assumptions")),
6869
outer_symbol_table(outer_symbol_table),
6970
ns(outer_symbol_table),
7071
target(_target),
@@ -212,14 +213,13 @@ class goto_symext
212213
// statistics
213214
unsigned total_vccs, remaining_vccs;
214215

215-
bool self_loops_to_assumptions;
216-
217216
/// language_mode: ID_java, ID_C or another language identifier
218217
/// if we know the source language in use, irep_idt() otherwise.
219218
irep_idt language_mode;
220219

221220
protected:
222221
const bool constant_propagation;
222+
const bool self_loops_to_assumptions;
223223

224224
/// The symbol table associated with the goto-program that we're
225225
/// executing. This symbol table will not additionally contain objects

0 commit comments

Comments
 (0)