diff --git a/regression/cbmc/Pointer_byte_extract8/main.i b/regression/cbmc/Pointer_byte_extract8/main.i deleted file mode 100644 index 0816108a607..00000000000 --- a/regression/cbmc/Pointer_byte_extract8/main.i +++ /dev/null @@ -1,40 +0,0 @@ -void *malloc(__CPROVER_size_t); - -typedef union -{ - int a; - int b; -} Union; - -typedef struct -{ - int Count; - 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; - - __CPROVER_assert(p->List[0].b==555, "p->List[0].b==555"); - __CPROVER_assert(p->List[0].a==555, "p->List[0].a==555"); - - // this should be fine - p->List[1].b = 999; - - __CPROVER_assert(p->List[1].b==999, "p->List[1].b==999"); - __CPROVER_assert(p->List[1].a==999, "p->List[1].a==999"); - - // this is out-of-bounds - p->List[2].a = 0; - - return 0; -} diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc deleted file mode 100644 index b23fa8bd0df..00000000000 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -KNOWNBUG -main.i ---bounds-check --32 --no-simplify -^EXIT=0$ -^SIGNAL=0$ -^\[main\.array_bounds\.5\] array.List upper bound: FAILED$ -^\*\* 1 of 9 failed --- -^warning: ignoring