Skip to content

Commit 587b361

Browse files
committed
Added a regression test for SMT encoding of struct
1 parent 4418acb commit 587b361

File tree

2 files changed

+25
-0
lines changed

2 files changed

+25
-0
lines changed

regression/cbmc/struct15/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
struct test
4+
{
5+
unsigned int a;
6+
unsigned int b;
7+
};
8+
9+
int main()
10+
{
11+
struct test t;
12+
if(t.a > 10)
13+
assert(t.a > 0);
14+
}

regression/cbmc/struct15/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--trace --smt2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^map::at:
9+
key not found
10+
--
11+
This test checks the encoding of C `struct`s using SMT2 data types.

0 commit comments

Comments
 (0)