@@ -61,15 +61,15 @@ static exprt c_get_nondet_bool(const typet &type)
61
61
62
62
class symbol_factoryt
63
63
{
64
- std::vector<symbolt const *> &symbols_created;
64
+ std::vector<const symbolt *> &symbols_created;
65
65
symbol_tablet &symbol_table;
66
66
const source_locationt &loc;
67
67
const bool assume_non_null;
68
68
namespacet ns;
69
69
70
70
public:
71
71
symbol_factoryt (
72
- std::vector<symbolt const *> &_symbols_created,
72
+ std::vector<const symbolt *> &_symbols_created,
73
73
symbol_tablet &_symbol_table,
74
74
const source_locationt &loc,
75
75
const bool _assume_non_null):
@@ -171,7 +171,7 @@ void symbol_factoryt::gen_nondet_init(
171
171
else
172
172
{
173
173
// Add the following code to assignments:
174
- // IF !( NONDET(_Bool) == FALSE ) THEN GOTO <label1>
174
+ // IF !NONDET(_Bool) THEN GOTO <label1>
175
175
// <expr> = <null pointer>
176
176
// GOTO <label2>
177
177
// <label1>: <expr> = &tmp$<temporary_counter>;
@@ -233,13 +233,15 @@ exprt c_nondet_symbol_factory(
233
233
main_symbol.name =identifier;
234
234
main_symbol.base_name =base_name;
235
235
main_symbol.type =type;
236
+ main_symbol.location =loc;
237
+
238
+ symbol_exprt main_symbol_expr=main_symbol.symbol_expr ();
236
239
237
240
symbolt *main_symbol_ptr;
238
241
bool moving_symbol_failed=symbol_table.move (main_symbol, main_symbol_ptr);
239
242
assert (!moving_symbol_failed);
240
243
241
- std::vector<symbolt const *> symbols_created;
242
- symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr ();
244
+ std::vector<const symbolt *> symbols_created;
243
245
symbols_created.push_back (main_symbol_ptr);
244
246
245
247
symbol_factoryt state (
@@ -252,7 +254,7 @@ exprt c_nondet_symbol_factory(
252
254
253
255
// Add the following code to init_code for each symbol that's been created:
254
256
// <type> <identifier>;
255
- for (symbolt const * symbol_ptr : symbols_created)
257
+ for (const symbolt * const symbol_ptr : symbols_created)
256
258
{
257
259
code_declt decl (symbol_ptr->symbol_expr ());
258
260
decl.add_source_location ()=loc;
0 commit comments