Remove undefined behaviour from pointer-byte-extract5

specifically the C90-style struct hack with non-flexible member.

Author: petr-bauch

regression/cbmc/Pointer_byte_extract5/main.i

@@ -11,13 +11,15 @@ typedef union
 typedef struct
 {
   int Count;
-  Union List[1];
+  // flexible array member -- note that smt conversion does not yet support
+  // 0-sized arrays
+  Union List[0];
 } Struct3;
 #pragma pack(pop)
 
 int main()
 {
-  Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union));
+  Struct3 *p = malloc(sizeof(Struct3) + 2 * sizeof(Union));
   p->Count = 3;
   int po=0;
 

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
@@ -10,5 +10,6 @@ array\.List dynamic object upper bound in p->List\[2\]: FAILURE
 --
 Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c.
 C90 did not have flexible arrays, and using arrays of size 1 was common
-practice: http://c-faq.com/struct/structhack.html. We need to treat those as if
-it were a zero-sized array.
+practice: http://c-faq.com/struct/structhack.html. But past C90 using
+non-flexible members for struct-hack is undefined, hence we changed the test to
+use flexible member instead.

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -10,5 +10,6 @@ array\.List dynamic object upper bound in p->List\[2\]: FAILURE
 --
 Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c.
 C90 did not have flexible arrays, and using arrays of size 1 was common
-practice: http://c-faq.com/struct/structhack.html. We need to treat those as if
-it were a zero-sized array.
+practice: http://c-faq.com/struct/structhack.html. But past C90 using
+non-flexible members for struct-hack is undefined, hence we changed the test to
+use flexible member instead.