Skip to content

Commit c9b37c7

Browse files
committed
Failing test documenting a case that 646cf29 missed
In 646cf29, initialisation of dynamic objects was added, but extern symbols were not considered.
1 parent 33561aa commit c9b37c7

File tree

2 files changed

+21
-0
lines changed

2 files changed

+21
-0
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+
KNOWNBUG
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.

0 commit comments

Comments
 (0)