Skip to content

Commit 698aebd

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 ddf416f commit 698aebd

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
@@ -60,9 +60,10 @@ class goto_symext
6060
doing_path_exploration(options.is_set("paths")),
6161
allow_pointer_unsoundness(
6262
options.get_bool_option("allow-pointer-unsoundness")),
63-
self_loops_to_assumptions(true),
6463
language_mode(),
6564
constant_propagation(options.get_bool_option("propagation")),
65+
self_loops_to_assumptions(
66+
options.get_bool_option("self-loops-to-assumptions")),
6667
outer_symbol_table(outer_symbol_table),
6768
ns(outer_symbol_table),
6869
target(_target),
@@ -210,14 +211,13 @@ class goto_symext
210211
// these bypass the target maps
211212
virtual void symex_step_goto(statet &, bool taken);
212213

213-
bool self_loops_to_assumptions;
214-
215214
/// language_mode: ID_java, ID_C or another language identifier
216215
/// if we know the source language in use, irep_idt() otherwise.
217216
irep_idt language_mode;
218217

219218
protected:
220219
const bool constant_propagation;
220+
const bool self_loops_to_assumptions;
221221

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

0 commit comments

Comments
 (0)