From e202df89d8c097b52c2514465d480f098945c9e6 Mon Sep 17 00:00:00 2001 From: Yumi Bagge Date: Fri, 6 Sep 2019 10:54:17 +0100 Subject: [PATCH] Add KNOWBUG test for 5093 --- .../main.c | 9 +++++++++ .../test.desc | 10 ++++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/main.c create mode 100644 regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc diff --git a/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/main.c b/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/main.c new file mode 100644 index 0000000000..dd15d90358 --- /dev/null +++ b/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/main.c @@ -0,0 +1,9 @@ +typedef struct ST +{ + int id; + int c[]; +} ST; + +void testFunc(ST **t) +{ +} diff --git a/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc b/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc new file mode 100644 index 0000000000..cf33b414d5 --- /dev/null +++ b/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--function testFunc +-- +^EXIT=0$ +^SIGNAL=0$ +-- +^EXIT=134$ +-- +Github issue #5093: Pointer to struct with flexible array member as parameter to entry point causes invariant violation