Make nondet-static replace lines in CPROVER_init

svorenova · svorenova · commit 1ea7e9e4cae1 · 2018-08-01T14:27:11.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
@@ -31,7 +31,7 @@ void nondet_static(
 
   Forall_goto_program_instructions(i_it, init)
   {
-    const goto_programt::instructiont &instruction=*i_it;
+    const goto_programt::instructiont instruction=*i_it;
 
     if(instruction.is_assign())
     {
@@ -54,7 +54,7 @@ void nondet_static(
       if(is_constant_or_has_constant_components(sym.type(), ns))
         continue;
 
-      i_it=init.insert_before(++i_it);
+      //i_it=init.insert_before(++i_it);
       i_it->make_assignment();
       i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
       i_it->source_location=instruction.source_location;

Original file line number	Diff line number	Diff line change
`@@ -31,7 +31,7 @@ void nondet_static(`
`31`	`31`
`32`	`32`	`Forall_goto_program_instructions(i_it, init)`
`33`	`33`	`{`
`34`		`- const goto_programt::instructiont &instruction=*i_it;`
	`34`	`+ const goto_programt::instructiont instruction=*i_it;`
`35`	`35`
`36`	`36`	`if(instruction.is_assign())`
`37`	`37`	`{`
`@@ -54,7 +54,7 @@ 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`	`+ //i_it=init.insert_before(++i_it);`
`58`	`58`	`i_it->make_assignment();`
`59`	`59`	`i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));`
`60`	`60`	`i_it->source_location=instruction.source_location;`