diff --git a/regression/cbmc/Function_Parameters1/main.c b/regression/cbmc/Function_Parameters1/main.c index 8f0d7dc515..29770c106d 100644 --- a/regression/cbmc/Function_Parameters1/main.c +++ b/regression/cbmc/Function_Parameters1/main.c @@ -1,9 +1,12 @@ +#include + void f(int, int array[*][*]); -void f(int size, int array[size][size]) +inline void f(int size, int array[size][++size]) { + assert(size==1001); assert(sizeof(array)==sizeof(int *)); - assert(sizeof(*array)==sizeof(int)*1000); + assert(sizeof(*array)==sizeof(int)*1001); } int main() diff --git a/regression/cbmc/Function_Parameters1/test.desc b/regression/cbmc/Function_Parameters1/test.desc index 466da18b2b..fc2b187405 100644 --- a/regression/cbmc/Function_Parameters1/test.desc +++ b/regression/cbmc/Function_Parameters1/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c ^EXIT=0$