Skip to content

Commit 2041736

Browse files
committed
Fix handling of extern symbols in phi_function
In 646cf29, initialisation of dynamic objects was added, but extern symbols were not considered. Includes a test that fails without this fix.
1 parent 33561aa commit 2041736

File tree

3 files changed

+23
-2
lines changed

3 files changed

+23
-2
lines changed

regression/cbmc/extern3/main.c

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
extern int x;
4+
5+
int main(int argc, char *argv[])
6+
{
7+
if(argc > 5)
8+
x = 42;
9+
10+
__CPROVER_assert(x == 42, "should fail");
11+
}

regression/cbmc/extern3/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
The change to phi_function of 646cf29941499 failed to consider the case of
10+
extern variables, which we leave uninitialised.

src/goto-symex/symex_goto.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -473,11 +473,11 @@ static void merge_names(
473473
rhs = goto_state_rhs;
474474
else if(goto_state.guard.is_false())
475475
rhs = dest_state_rhs;
476-
else if(goto_count == 0)
476+
else if(goto_count == 0 && symbol.value.is_not_nil())
477477
{
478478
rhs = dest_state_rhs;
479479
}
480-
else if(dest_count == 0)
480+
else if(dest_count == 0 && symbol.value.is_not_nil())
481481
{
482482
rhs = goto_state_rhs;
483483
}

0 commit comments

Comments
 (0)