Make nondet-static replace lines in CPROVER_init

svorenova · svorenova · commit bd46eee42a63 · 2018-08-01T16:10:14.000+01:00
Instead of adding a new line that nondet initializes a variable after
the original line that sets it, we now replace the original one
diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp
@@ -52,11 +52,11 @@ void nondet_static(
       if(is_constant_or_has_constant_components(sym.type(), ns))
         continue;
 
-      i_it=init.insert_before(++i_it);
+      const goto_programt::instructiont original_instruction = instruction;
       i_it->make_assignment();
       i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
-      i_it->source_location=instruction.source_location;
-      i_it->function=instruction.function;
+      i_it->source_location = original_instruction.source_location;
+      i_it->function = original_instruction.function;
     }
     else if(instruction.is_function_call())
     {

Original file line number	Diff line number	Diff line change
`@@ -52,11 +52,11 @@ void nondet_static(`
`52`	`52`	`if(is_constant_or_has_constant_components(sym.type(), ns))`
`53`	`53`	`continue;`
`54`	`54`
`55`		`- i_it=init.insert_before(++i_it);`
	`55`	`+ const goto_programt::instructiont original_instruction = instruction;`
`56`	`56`	`i_it->make_assignment();`
`57`	`57`	`i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));`
`58`		`- i_it->source_location=instruction.source_location;`
`59`		`- i_it->function=instruction.function;`
	`58`	`+ i_it->source_location = original_instruction.source_location;`
	`59`	`+ i_it->function = original_instruction.function;`
`60`	`60`	`}`
`61`	`61`	`else if(instruction.is_function_call())`
`62`	`62`	`{`