diff --git a/regression/cbmc/Pointer_byte_extract8/main.i b/regression/cbmc/Pointer_byte_extract8/main.i index 0816108a607..164f8f1fed3 100644 --- a/regression/cbmc/Pointer_byte_extract8/main.i +++ b/regression/cbmc/Pointer_byte_extract8/main.i @@ -12,14 +12,11 @@ typedef struct Union List[1]; } __attribute__((packed)) Struct3; -extern size_t __CPROVER_malloc_size; - int main() { Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union)); p->Count = 3; int po=0; - size_t m=__CPROVER_malloc_size; // this should be fine p->List[0].a = 555; diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc index b23fa8bd0df..5373ac6f3d6 100644 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ b/regression/cbmc/Pointer_byte_extract8/test.desc @@ -1,9 +1,9 @@ -KNOWNBUG +CORE main.i --bounds-check --32 --no-simplify -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^\[main\.array_bounds\.5\] array.List upper bound: FAILED$ -^\*\* 1 of 9 failed +^\[main\.array_bounds\..*\] array.List dynamic object upper bound .*: FAILURE$ +^\*\* 1 of .* failed -- ^warning: ignoring