Do not assign to objects that have gone out of scope
Pointer dereferencing may yield objects that have meanwhile gone out of scope. Assigning to them is unnecessary, and performing a merge on those would yield inconsistent equations (as witnessed by the included regression test). Filtering out the merge in phi nodes is not easily possible as there are several cases where it is permissible that only one of the states entering the phi node has an (L1) object, such as declarations only seen in one branch. Fixes: #1115
This commit is contained in:
parent
32b68ced26
commit
369f077d2e
|
@ -0,0 +1,24 @@
|
|||
unsigned int *GLOBAL_POINTER[1];
|
||||
|
||||
int index;
|
||||
|
||||
void f(void)
|
||||
{
|
||||
unsigned int actual=0u;
|
||||
GLOBAL_POINTER[0] = &actual;
|
||||
|
||||
if(index==0)
|
||||
*GLOBAL_POINTER[index] = 1u;
|
||||
else
|
||||
actual = 2u;
|
||||
|
||||
__CPROVER_assume(1u == actual);
|
||||
}
|
||||
|
||||
void main(void)
|
||||
{
|
||||
index=nondet_int();
|
||||
f();
|
||||
f();
|
||||
__CPROVER_assert(0==1, "");
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -209,6 +209,17 @@ void goto_symext::symex_assign_symbol(
|
|||
guardt &guard,
|
||||
assignment_typet assignment_type)
|
||||
{
|
||||
// do not assign to L1 objects that have gone out of scope --
|
||||
// pointer dereferencing may yield such objects; parameters do not
|
||||
// have an L2 entry set up beforehand either, so exempt them from
|
||||
// this check (all other L1 objects should have seen a declaration)
|
||||
const symbolt *s;
|
||||
if(!ns.lookup(lhs.get_object_name(), s) &&
|
||||
!s->is_parameter &&
|
||||
!lhs.get_level_1().empty() &&
|
||||
state.level2.current_count(lhs.get_identifier())==0)
|
||||
return;
|
||||
|
||||
exprt ssa_rhs=rhs;
|
||||
|
||||
// put assignment guard into the rhs
|
||||
|
|
Loading…
Reference in New Issue