diff --git a/regression/cbmc-concurrency/thread_local2/main.c b/regression/cbmc-concurrency/thread_local2/main.c new file mode 100644 index 00000000000..a2a67473b9d --- /dev/null +++ b/regression/cbmc-concurrency/thread_local2/main.c @@ -0,0 +1,11 @@ +int __CPROVER_thread_local thlocal = 4; + +int main() +{ + int loc; + + loc = 123; + +__CPROVER_ASYNC_3: + thlocal = loc, __CPROVER_assert(thlocal == 123, "hello"); +} diff --git a/regression/cbmc-concurrency/thread_local2/test.desc b/regression/cbmc-concurrency/thread_local2/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc-concurrency/thread_local2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/extern3/main.c b/regression/cbmc/extern3/main.c new file mode 100644 index 00000000000..0b623409d55 --- /dev/null +++ b/regression/cbmc/extern3/main.c @@ -0,0 +1,11 @@ +#include + +extern int x; + +int main(int argc, char *argv[]) +{ + if(argc > 5) + x = 42; + + __CPROVER_assert(x == 42, "should fail"); +} diff --git a/regression/cbmc/extern3/test.desc b/regression/cbmc/extern3/test.desc new file mode 100644 index 00000000000..578c27b1fa2 --- /dev/null +++ b/regression/cbmc/extern3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +The change to phi_function of 646cf29941499 failed to consider the case of +extern variables, which we leave uninitialised. diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 9297145c1f5..fde8a2b3bdb 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -218,17 +218,6 @@ 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 diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 05429aa412d..3823cfecff0 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -423,7 +423,14 @@ static void merge_names( if(goto_count == dest_count) return; // not at all changed - // changed! + // changed - but only on a branch that is now dead, and the other branch is + // uninitialized/invalid + if( + (dest_state.guard.is_false() && goto_count == 0) || + (goto_state.guard.is_false() && dest_count == 0)) + { + return; + } // shared variables are renamed on every access anyway, we don't need to // merge anything @@ -473,11 +480,11 @@ static void merge_names( rhs = goto_state_rhs; else if(goto_state.guard.is_false()) rhs = dest_state_rhs; - else if(goto_count == 0) + else if(goto_count == 0 && symbol.value.is_not_nil()) { rhs = dest_state_rhs; } - else if(dest_count == 0) + else if(dest_count == 0 && symbol.value.is_not_nil()) { rhs = goto_state_rhs; }