Create SSA-level 2 names for individual fields
During symex, a declaration introduces non-deterministic values for the declared symbol by creating a fresh L2 name without assigning any value to it. With field-sensitive SSA, the same must be done for each field (just like we already did the inverse for objects going out of scope via a DEAD instruction).
This commit is contained in:
parent
6c8954b8db
commit
24f4674084
|
@ -0,0 +1,14 @@
|
|||
struct S
|
||||
{
|
||||
int x;
|
||||
};
|
||||
|
||||
int main(int argc, char *argv[])
|
||||
{
|
||||
struct S s;
|
||||
|
||||
if(argc > 3)
|
||||
s.x = 42;
|
||||
|
||||
__CPROVER_assert(s.x == 42, "should fail");
|
||||
}
|
|
@ -0,0 +1,11 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
With field-sensitive SSA encoding we need to make sure that each struct member
|
||||
is treated as non-deterministic unless initialised.
|
|
@ -64,8 +64,17 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
|
|||
}
|
||||
|
||||
// L2 renaming
|
||||
std::size_t generation = state.increase_generation(l1_identifier, ssa);
|
||||
CHECK_RETURN(generation == 1);
|
||||
const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
|
||||
std::set<symbol_exprt> fields_set;
|
||||
find_symbols(fields, fields_set);
|
||||
|
||||
for(const auto &l1_symbol : fields_set)
|
||||
{
|
||||
ssa_exprt field_ssa = to_ssa_expr(l1_symbol);
|
||||
std::size_t field_generation =
|
||||
state.increase_generation(l1_symbol.get_identifier(), field_ssa);
|
||||
CHECK_RETURN(field_generation == 1);
|
||||
}
|
||||
|
||||
const bool record_events=state.record_events;
|
||||
state.record_events=false;
|
||||
|
|
Loading…
Reference in New Issue