Fix for the constant arrays marked as nondet issue.

regression/cbmc/no_nondet_static/main.c

@@ -0,0 +1,69 @@
+int x;
+int y = 23;
+const int z = 23;
+
+struct s { int x; };
+struct s s1;
+struct s s2 = { 23 };
+const struct s s3 = { 23 };
+
+struct t { int x; const int y; };
+struct t t1;
+struct t t2 = { 23, 23 };
+const struct t t3 = { 23, 23 };
+
+struct u { const int x; };
+struct u u1;
+struct u u2 = { 23 };
+const struct u u3 = { 23 };
+
+struct contains_pointer {  int x; int *p; };
+// const int *p : declare p as pointer to const int
+struct contains_pointer_to_const {  int x; const int *p; };
+// int * const p : declare p as const pointer to int
+struct contains_constant_pointer {  int x; int * const p; };
+
+struct contains_pointer a[3] = { {23, &x}, {23, &x}, {23, &x} };
+struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
+struct contains_pointer_to_const c[3] = { {23, &z}, {23, &z}, {23, &z} };
+
+typedef int Int;
+typedef const int Const_Int;
+
+const Int p = 23;
+Const_Int q = 23;
+
+
+#include <assert.h>
+
+int main (int argc, char **argv) 
+{  
+  /* Pass normally but fail with nondet-static */
+  assert(x == 0);
+  assert(y == 23);
+  assert(s1.x == 0);
+  assert(s2.x == 23);
+  assert(a[0].x == 23);
+  assert(a[0].p == &x);
+  assert(c[2].x == 23);
+  assert(c[2].p == &z);
+
+  /* Should still pass */
+  assert(z == 23);
+  assert(s3.x == 23);
+  assert(t1.y == 0);
+  assert(t2.y == 23);
+  assert(t3.x == 23);
+  assert(t3.y == 23);
+  assert(u1.x == 0);
+  assert(u2.x == 23);
+  assert(u3.x == 23);
+  assert(p == 23);
+  assert(q == 23);
+  assert(t1.x == 0);
+  assert(t2.x == 23);
+  assert(b[1].x == 23);
+  assert(b[1].p == &y);
+
+  return 0;
+}

regression/cbmc/no_nondet_static/test.desc

@@ -0,0 +1,29 @@
+CORE
+main.c
+--nondet-static
+^VERIFICATION FAILED$
+assertion x == 0: FAILURE
+assertion y == 23: FAILURE
+assertion s1.x == 0: FAILURE
+assertion s2.x == 23: FAILURE
+assertion a\[0\].x == 23: FAILURE
+assertion a\[0\].p == &x: FAILURE
+assertion c\[2\].x == 23: FAILURE
+assertion c\[2\].p == &z: FAILURE
+assertion z == 23: SUCCESS
+assertion s3.x == 23: SUCCESS
+assertion t1.y == 0: SUCCESS
+assertion t2.y == 23: SUCCESS
+assertion t3.x == 23: SUCCESS
+assertion t3.y == 23: SUCCESS
+assertion u1.x == 0: SUCCESS
+assertion u2.x == 23: SUCCESS
+assertion u3.x == 23: SUCCESS
+assertion p == 23: SUCCESS
+assertion q == 23: SUCCESS
+assertion t1.x == 0: SUCCESS
+assertion t2.x == 23: SUCCESS
+assertion b\[1\].x == 23: SUCCESS
+assertion b\[1\].p == &y: SUCCESS
+--
+--

src/goto-instrument/nondet_static.cpp

@@ -18,6 +18,7 @@ Date: November 2011
 #include <util/std_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
+#include <util/type.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/goto_functions.h>
@@ -51,7 +52,7 @@ void nondet_static(
         continue;
 
       // constant?
-      if(sym.type().get_bool(ID_C_constant))
+      if(is_constant_or_has_constant_components(sym.type(), ns))
         continue;
 
       i_it=init.insert_before(++i_it);

src/util/type.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 
 #include "type.h"
+#include "std_types.h"
+#include "namespace.h"
 
 void typet::copy_to_subtypes(const typet &type)
 {
@@ -34,3 +36,72 @@ bool is_number(const typet &type)
          id==ID_floatbv ||
          id==ID_fixedbv;
 }
+
+/// Identify if a given type is constant itself or
+/// contains constant components. Examples include:
+///  - const int a;
+///  - struct contains_constant_pointer {  int x; int * const p; };
+///  - const int b[3];
+/// \param type The type we want to query constness of.
+/// \param ns The namespace, needed for resolution of symbols.
+/// \return Whether passed in type is const or not.
+bool is_constant_or_has_constant_components(
+  const typet &type, const namespacet &ns)
+{
+  // Helper function to avoid the code duplication
+  // in the branches below.
+  const auto has_constant_components =
+  [](const typet &subtype) -> bool
+  {
+    if(subtype.id() == ID_struct || subtype.id() == ID_union)
+    {
+      const auto &struct_union_type = to_struct_union_type(subtype);
+      for(const auto &component : struct_union_type.components())
+      {
+        if(component.type().id() == ID_pointer)
+          return component.type().get_bool(ID_C_constant);
+        if(component.type().get_bool(ID_C_constant))
+          return true;
+      }
+    }
+    return false;
+  };
+
+  // There are 3 possibilities the code below is handling.
+  // The possibilities are enumerated as comments, to show
+  // what each code is supposed to be handling. For more
+  // comprehensive test case for this, take a look at
+  // regression/cbmc/no_nondet_static/main.c
+
+  // const int a;
+  if(type.get_bool(ID_C_constant))
+    return true;
+
+  // When we have a case like the following, we don't immediately
+  // see the struct t. Instead, we only get to see symbol t1, which
+  // we have to use the namespace to resolve to its definition:
+  // struct t { const int a; };
+  // struct t t1;
+  if(type.id() == ID_symbol)
+  {
+    const auto &subtype = ns.follow(type);
+    return has_constant_components(subtype);
+  }
+
+  // In a case like this, were we see an array (b[3] here), we know that
+  // the array contains subtypes. We get the first one, and
+  // then resolve it to its  definition through the usage of the namespace.
+  // struct contains_constant_pointer { int x; int * const p; };
+  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
+  if(type.has_subtype())
+  {
+    const auto &subtype = type.subtype();
+    if(subtype.id() == ID_symbol)
+    {
+      const auto &new_subtype = ns.follow(to_symbol_type(subtype));
+      return has_constant_components(new_subtype);
+    }
+  }
+
+  return false;
+}

src/util/type.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_TYPE_H
 
 #include <util/source_location.h>
+#include "namespace.h"
 
 #define SUBTYPE_IN_GETSUB
 #define SUBTYPES_IN_GETSUB
@@ -203,4 +204,9 @@ pre-defined types:
 bool is_number(const typet &type);
 // rational, real, integer, complex, unsignedbv, signedbv, floatbv
 
+// Is the passed in type const qualified?
+bool is_constant_or_has_constant_components(
+    const typet &type,
+    const namespacet &ns);
+
 #endif // CPROVER_UTIL_TYPE_H