Remove undefined behaviour from pointer-byte-extract5

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

We also update the number of succeeding assertions because there is now an extra
upper bound check for accessing the 0th element of `List`.

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/test.desc

@@ -4,11 +4,12 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed 
+\*\* 1 of \d+ failed
 --
 ^warning: ignoring
 --
 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.