Make nondet-static replace lines in CPROVER_init

svorenova · svorenova · commit ec4d5cdd6a30 · 2018-08-02T12:31:12.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
@@ -54,11 +54,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
`@@ -54,11 +54,11 @@ void nondet_static(`
`54`	`54`	`if(is_constant_or_has_constant_components(sym.type(), ns))`
`55`	`55`	`continue;`
`56`	`56`
`57`		`- i_it=init.insert_before(++i_it);`
	`57`	`+ const goto_programt::instructiont original_instruction = instruction;`
`58`	`58`	`i_it->make_assignment();`
`59`	`59`	`i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));`
`60`		`- i_it->source_location=instruction.source_location;`
`61`		`- i_it->function=instruction.function;`
	`60`	`+ i_it->source_location = original_instruction.source_location;`
	`61`	`+ i_it->function = original_instruction.function;`
`62`	`62`	`}`
`63`	`63`	`else if(instruction.is_function_call())`
`64`	`64`	`{`