Fix handling of extern symbols in phi_function

In 646cf29941, initialisation of dynamic objects was added, but extern
symbols were not considered. Includes a test that fails without this fix.
This commit is contained in:
Michael Tautschnig 2018-12-19 12:21:39 +00:00
parent 5594db6417
commit e743f02fc3
3 changed files with 23 additions and 2 deletions

View File

@ -0,0 +1,11 @@
#include <assert.h>
extern int x;
int main(int argc, char *argv[])
{
if(argc > 5)
x = 42;
__CPROVER_assert(x == 42, "should fail");
}

View File

@ -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.

View File

@ -473,11 +473,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;
}