Skip to content

Commit 9327fd8

Browse files
committed
Add missing test description file
When adding the test in 6b09359 I had likely failed to do `git add` on test.desc, and instead just added the C file. This commit now rectifies that.
1 parent 57c59fc commit 9327fd8

File tree

1 file changed

+13
-0
lines changed
  • regression/cbmc/empty_compound_type3

1 file changed

+13
-0
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE broken-smt-backend
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring
9+
Invariant check failed
10+
--
11+
Taking the address of an empty struct resulted in an invariant failure in
12+
address-of flattening. This test was generated using C-Reduce plus some further
13+
manual simplification.

0 commit comments

Comments
 (0)