Skip to content

Commit e9b5146

Browse files
committed
Add regression test for cbmc crash in flattening
1 parent 5aa4b14 commit e9b5146

File tree

2 files changed

+18
-0
lines changed

2 files changed

+18
-0
lines changed

regression/cbmc/r_w_ok_bug/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
void main()
5+
{
6+
char *p1;
7+
__CPROVER_assume(__CPROVER_r_ok(p1 - 1, 1));
8+
*p1;
9+
}

regression/cbmc/r_w_ok_bug/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
main.c
3+
--pointer-check --no-simplify --no-propagation
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Crashes during the flattening

0 commit comments

Comments
 (0)