Skip to content

Commit e202df8

Browse files
committed
Add KNOWBUG test for 5093
1 parent fc0a0cd commit e202df8

File tree

2 files changed

+19
-0
lines changed
  • regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point

2 files changed

+19
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
typedef struct ST
2+
{
3+
int id;
4+
int c[];
5+
} ST;
6+
7+
void testFunc(ST **t)
8+
{
9+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
main.c
3+
--function testFunc
4+
--
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^EXIT=134$
9+
--
10+
Github issue #5093: Pointer to struct with flexible array member as parameter to entry point causes invariant violation

0 commit comments

Comments
 (0)