diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 2b51ce8fb05..105af6a2213 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -61,7 +61,7 @@ static exprt c_get_nondet_bool(const typet &type) class symbol_factoryt { - std::vector &symbols_created; + std::vector &symbols_created; symbol_tablet &symbol_table; const source_locationt &loc; const bool assume_non_null; @@ -69,7 +69,7 @@ class symbol_factoryt public: symbol_factoryt( - std::vector &_symbols_created, + std::vector &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null): @@ -125,7 +125,7 @@ exprt symbol_factoryt::allocate_object( // = &tmp$ code_assignt assign(target_expr, aoe); assign.add_source_location()=loc; - assignments.add(assign); + assignments.move(assign); return aoe; } @@ -171,7 +171,7 @@ void symbol_factoryt::gen_nondet_init( else { // Add the following code to assignments: - // IF !(NONDET(_Bool) == FALSE) THEN GOTO + // IF !NONDET(_Bool) THEN GOTO // = // GOTO // : = &tmp$; @@ -186,7 +186,7 @@ void symbol_factoryt::gen_nondet_init( null_check.then_case()=set_null_inst; null_check.else_case()=non_null_inst; - assignments.add(null_check); + assignments.move(null_check); } } // TODO(OJones): Add support for structs and arrays @@ -202,7 +202,7 @@ void symbol_factoryt::gen_nondet_init( code_assignt assign(expr, rhs); assign.add_source_location()=loc; - assignments.add(assign); + assignments.move(assign); } } @@ -233,13 +233,15 @@ exprt c_nondet_symbol_factory( main_symbol.name=identifier; main_symbol.base_name=base_name; main_symbol.type=type; + main_symbol.location=loc; + + symbol_exprt main_symbol_expr=main_symbol.symbol_expr(); symbolt *main_symbol_ptr; bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr); assert(!moving_symbol_failed); - std::vector symbols_created; - symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr(); + std::vector symbols_created; symbols_created.push_back(main_symbol_ptr); symbol_factoryt state( @@ -252,11 +254,11 @@ exprt c_nondet_symbol_factory( // Add the following code to init_code for each symbol that's been created: // ; - for(symbolt const *symbol_ptr : symbols_created) + for(const symbolt * const symbol_ptr : symbols_created) { code_declt decl(symbol_ptr->symbol_expr()); decl.add_source_location()=loc; - init_code.add(decl); + init_code.move(decl); } init_code.append(assignments); @@ -273,7 +275,7 @@ exprt c_nondet_symbol_factory( from_integer(0, index_type()))); input_code.op1()=symbol_ptr->symbol_expr(); input_code.add_source_location()=loc; - init_code.add(input_code); + init_code.move(input_code); } return main_symbol_expr; diff --git a/src/util/std_code.h b/src/util/std_code.h index cd017a658ba..eed132a71dd 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -78,6 +78,11 @@ class code_blockt:public codet o.push_back(*it); } + void move(codet &code) + { + move_to_operands(code); + } + void add(const codet &code) { copy_to_operands(code);