Use bddt to simplify guardt

CODING_STANDARD.md

@@ -107,6 +107,9 @@ Here a few minimalistic coding rules for the CPROVER source tree.
   include in the source file. For example, given `foo.h` and `foo.cpp`, the
   line `#include "foo.h"` should precede all other include statements in
   `foo.cpp`.
+- Use the C++ versions of C headers (e.g. `cmath` instead of `math.h`).
+  Some of the C headers use macros instead of functions which can have
+  unexpected consequences.
 
 # Makefiles
 - Each source file should appear on a separate line

regression/ansi-c/Struct_Initialization1/main.c

@@ -1,13 +1,19 @@
 #define STATIC_ASSERT(condition) \
   int some_array##__LINE__[(condition) ? 1 : -1]
 
+struct A {
+  int x;
+  int y;
+};
+
 struct _classinfo {
   char a;
+  struct A s;
   int *interfaces[];
 };
 
-struct _classinfo nullclass1 = { 42, 0, 0 };
-struct _classinfo nullclass2 = { 42, { 0, 0 } };
+struct _classinfo nullclass1 = { 42, 1, 2, 3, 4 };
+struct _classinfo nullclass2 = { 42, { 1, 2 }, { 3, 4 } };
 
 STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo));
 STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo));

regression/ansi-c/Struct_Initialization1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/ansi-c/Struct_Initialization2/main.c

@@ -0,0 +1,24 @@
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1]
+
+struct A {
+  int x;
+  int y;
+  int arr[];
+};
+
+struct _classinfo {
+  char a;
+  struct A s;
+  int *interfaces[];
+};
+
+struct _classinfo nullclass1 = { 42, 1, 2, 0, 3, 4 };
+struct _classinfo nullclass2 = { 42, { 1, 2, 0 }, { 3, 4 } };
+
+STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo));
+STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo));
+
+int main()
+{
+}

regression/ansi-c/Struct_Initialization2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
+--
+variable-length arrays in the middle of a struct are not permitted

regression/cbmc/dynamic_size1/main.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int main()
+{
+  unsigned x;
+
+  int *A=malloc(x*sizeof(int));
+
+  char *p=&A[1];
+
+  char c=*p;
+
+  return c;
+}

regression/cbmc/dynamic_size1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^unknown or invalid type size:

regression/cbmc/fgets1/main.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  char buffer[3]={'a', 'b', '\0'};
+  FILE *f=fdopen(0, "r");
+  if(!f)
+    return 1;
+
+  char *p=fgets(buffer, 3, f);
+  if(p)
+  {
+    assert(buffer[1]==p[1]);
+    assert(buffer[2]=='\0');
+    assert(p[1]=='b'); // expected to fail
+  }
+
+  fclose(f);
+
+  return 0;
+}

regression/cbmc/fgets1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
+\*\* 1 of 38 failed \(2 iterations\)
+--
+^warning: ignoring

regression/cbmc/union9/main.c

@@ -0,0 +1,35 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+typedef union {
+  struct {
+    uint8_t x;
+    uint8_t z;
+  } b;
+} union_t;
+
+typedef struct {
+    uint32_t magic;
+    union_t unions[];
+} flex;
+
+int flex_init(flex * flex, size_t num)
+{
+    if (num == 0 || num >= 200) {
+        return -1;
+    }
+    flex->unions[num - 1].b.z = 255;
+    return 0;
+}
+
+int main() {
+    uint8_t num = nondet_size();
+    flex * pool = (flex *) malloc(sizeof(flex) + num * sizeof(union_t));
+    int ret = flex_init(pool, num);
+    if (num > 0 && num < 200) {
+        __CPROVER_assert(ret == 0, "Accept inside range");
+    } else {
+        __CPROVER_assert(ret != 0, "Reject outside range");
+    }
+}
+

regression/cbmc/union9/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_base.h

@@ -89,10 +89,11 @@ class c_typecheck_baset:
     const typet &type,
     bool force_constant);
 
-  virtual void do_designated_initializer(
+  virtual exprt::operandst::const_iterator do_designated_initializer(
     exprt &result,
     designatort &designator,
-    const exprt &value,
+    const exprt &initializer_list,
+    exprt::operandst::const_iterator init_it,
     bool force_constant);
 
   designatort make_designator(const typet &type, const exprt &src);

src/ansi-c/c_typecheck_initializer.cpp

@@ -256,9 +256,7 @@ void c_typecheck_baset::designator_enter(
   const typet &type,
   designatort &designator)
 {
-  designatort::entryt entry;
-  entry.type=type;
-  entry.index=0;
+  designatort::entryt entry(type);
 
   const typet &full_type=follow(type);
 
@@ -268,6 +266,8 @@ void c_typecheck_baset::designator_enter(
 
     entry.size=struct_type.components().size();
     entry.subtype.make_nil();
+    // only a top-level struct may end with a variable-length array
+    entry.vla_permitted=designator.empty();
 
     for(struct_typet::componentst::const_iterator
         it=struct_type.components().begin();
@@ -351,12 +351,16 @@ void c_typecheck_baset::designator_enter(
 
 /// \param pre:initialized result, designator
 /// \return sets result
-void c_typecheck_baset::do_designated_initializer(
+exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
   exprt &result,
   designatort &designator,
-  const exprt &value,
+  const exprt &initializer_list,
+  exprt::operandst::const_iterator init_it,
   bool force_constant)
 {
+  // copy the value, we may need to adjust it
+  exprt value=*init_it;
+
   assert(!designator.empty());
 
   if(value.id()==ID_designated_initializer)
@@ -370,8 +374,10 @@ void c_typecheck_baset::do_designated_initializer(
 
     assert(!designator.empty());
 
-    return do_designated_initializer(
-      result, designator, value.op0(), force_constant);
+    // discard the return value
+    do_designated_initializer(
+      result, designator, value, value.operands().begin(), force_constant);
+    return ++init_it;
   }
 
   exprt *dest=&result;
@@ -503,7 +509,7 @@ void c_typecheck_baset::do_designated_initializer(
 
       assert(full_type==follow(dest->type()));
 
-      return; // done
+      return ++init_it; // done
     }
 
     // union? The component in the zero initializer might
@@ -537,7 +543,7 @@ void c_typecheck_baset::do_designated_initializer(
     if(value.id()==ID_initializer_list)
     {
       *dest=do_initializer_rec(value, type, force_constant);
-      return; // done
+      return ++init_it; // done
     }
     else if(value.id()==ID_string_constant)
     {
@@ -549,7 +555,7 @@ void c_typecheck_baset::do_designated_initializer(
           follow(full_type.subtype()).id()==ID_unsignedbv))
       {
         *dest=do_initializer_rec(value, type, force_constant);
-        return; // done
+        return ++init_it; // done
       }
     }
     else if(follow(value.type())==full_type)
@@ -562,7 +568,7 @@ void c_typecheck_baset::do_designated_initializer(
          full_type.id()==ID_vector)
       {
         *dest=value;
-        return; // done
+        return ++init_it; // done
       }
     }
 
@@ -574,21 +580,49 @@ void c_typecheck_baset::do_designated_initializer(
     // we are initializing a compound type, and enter it!
     // this may change the type, full_type might not be valid any more
     const typet dest_type=full_type;
+    const bool vla_permitted=designator.back().vla_permitted;
     designator_enter(type, designator);
 
+    // GCC permits (though issuing a warning with -Wall) composite
+    // types built from flat initializer lists
     if(dest->operands().empty())
     {
-      err_location(value);
-      error() << "cannot initialize type `"
-              << to_string(dest_type) << "' using value `"
-              << to_string(value) << "'" << eom;
-      throw 0;
+      warning().source_location=value.find_source_location();
+      warning() << "initialisation of " << full_type.id()
+                << " requires initializer list, found "
+                << value.id() << " instead" << eom;
+
+      // in case of a variable-length array consume all remaining
+      // initializer elements
+      if(vla_permitted &&
+         dest_type.id()==ID_array &&
+         (to_array_type(dest_type).size().is_zero() ||
+          to_array_type(dest_type).size().is_nil()))
+      {
+        value.id(ID_initializer_list);
+        value.operands().clear();
+        for( ; init_it!=initializer_list.operands().end(); ++init_it)
+          value.copy_to_operands(*init_it);
+        *dest=do_initializer_rec(value, dest_type, force_constant);
+
+        return init_it;
+      }
+      else
+      {
+        err_location(value);
+        error() << "cannot initialize type `"
+          << to_string(dest_type) << "' using value `"
+          << to_string(value) << "'" << eom;
+        throw 0;
+      }
     }
 
     dest=&(dest->op0());
 
     // we run into another loop iteration
   }
+
+  return ++init_it;
 }
 
 void c_typecheck_baset::increment_designator(designatort &designator)
@@ -651,8 +685,7 @@ designatort c_typecheck_baset::make_designator(
   forall_operands(it, src)
   {
     const exprt &d_op=*it;
-    designatort::entryt entry;
-    entry.type=type;
+    designatort::entryt entry(type);
     const typet &full_type=follow(entry.type);
 
     if(full_type.id()==ID_array)
@@ -856,10 +889,12 @@ exprt c_typecheck_baset::do_initializer_list(
 
   designator_enter(type, current_designator);
 
-  forall_operands(it, value)
+  const exprt::operandst &operands=value.operands();
+  for(exprt::operandst::const_iterator it=operands.begin();
+      it!=operands.end(); ) // no ++it
   {
-    do_designated_initializer(
-      result, current_designator, *it, force_constant);
+    it=do_designated_initializer(
+      result, current_designator, value, it, force_constant);
 
     // increase designator -- might go up
     increment_designator(current_designator);

src/ansi-c/designator.h

@@ -24,9 +24,11 @@ class designatort
   {
     size_t index;
     size_t size;
+    bool vla_permitted;
     typet type, subtype;
 
-    entryt():index(0), size(0)
+    explicit entryt(const typet &type):
+      index(0), size(0), vla_permitted(false), type(type)
     {
     }
   };