Skip to content

Commit 42e3acf

Browse files
author
svorenova
committed
Make nondet-static replace lines in CPROVER_init
Instead of keeping both the original line that sets the value of a variable and the new line that nondet initializes it, we only keep the new one
1 parent b62bf01 commit 42e3acf

File tree

1 file changed

+8
-5
lines changed

1 file changed

+8
-5
lines changed

src/goto-instrument/nondet_static.cpp

+8-5
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Date: November 2011
1616

1717
#include <goto-programs/goto_model.h>
1818

19+
#include <goto-programs/remove_skip.h>
1920
#include <linking/static_lifetime_init.h>
2021

2122
void nondet_static(
@@ -58,11 +59,12 @@ void nondet_static(
5859
if(is_constant_or_has_constant_components(sym.type(), ns))
5960
continue;
6061

61-
i_it=init.insert_before(++i_it);
62-
i_it->make_assignment();
63-
i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
64-
i_it->source_location=instruction.source_location;
65-
i_it->function=instruction.function;
62+
const auto &ni_it = init.insert_before(++i_it);
63+
ni_it->make_assignment();
64+
ni_it->code = code_assignt(sym, side_effect_expr_nondett(sym.type()));
65+
ni_it->source_location = instruction.source_location;
66+
ni_it->function = instruction.function;
67+
i_it->make_skip();
6668
}
6769
else if(instruction.is_function_call())
6870
{
@@ -73,6 +75,7 @@ void nondet_static(
7375
nondet_static(ns, goto_functions, fsym.get_identifier());
7476
}
7577
}
78+
remove_skip(init);
7679
}
7780

7881
void nondet_static(

0 commit comments

Comments
 (0)