Skip to content

Commit 5b3c82d

Browse files
authored
Merge pull request #5094 from yumibagge/yb/cbmc-regression-knownbug-5093
Add KNOWBUG test for 5093
2 parents 7bcabb2 + e202df8 commit 5b3c82d

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)