Merge pull request #1146 from tautschnig/fix-525

Do not accept arrays of variable size with static lifetime

Author: Daniel Kroening

regression/ansi-c/Array_Declarator8/main.c

@@ -0,0 +1,20 @@
+typedef unsigned char u1;
+typedef unsigned short u2;
+typedef unsigned long long u4;
+
+// Not resolved (as expected)
+u4 B[( (u1)( ( (u1)15 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)15)) > ((u1)64)) ? (0) : (1) ) ) )];
+
+// Correctly resolved
+u2 C[( (u1)( ( (u1)11 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)11)) > ((u1)64)) ? (0) : (1) ) ) )];
+
+int main()
+{
+  // Correctly resolved
+  u2 A[( (u1)( ( (u1)1 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)1)) > ((u1)64)) ? (0) : (1) ) ) )];
+
+  // Correctly resolved
+  static u4 D[( (u1)( ( (u1)4 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)4)) > ((u1)64)) ? (0) : (1) ) ) )];
+
+  return 0;
+}

regression/ansi-c/Array_Declarator8/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+array size of static symbol `B' is not constant$
+--
+^warning: ignoring

src/ansi-c/ansi_c_declaration.cpp

@@ -128,6 +128,7 @@ void ansi_c_declarationt::to_symbol(
   symbol.value=declarator.value();
   symbol.type=full_type(declarator);
   symbol.name=declarator.get_name();
+  symbol.pretty_name=symbol.name;
   symbol.base_name=declarator.get_base_name();
   symbol.is_type=get_is_typedef();
   symbol.location=declarator.source_location();

src/ansi-c/c_typecheck_base.cpp

@@ -45,8 +45,6 @@ void c_typecheck_baset::move_symbol(symbolt &symbol, symbolt *&new_symbol)
 
 void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
 {
-  current_symbol_id=symbol.name;
-
   bool is_function=symbol.type.id()==ID_code;
 
   const typet &final_type=follow(symbol.type);
@@ -703,6 +701,7 @@ void c_typecheck_baset::typecheck_declaration(
 
       symbolt symbol;
       declaration.to_symbol(*d_it, symbol);
+      current_symbol=symbol;
 
       // now check other half of type
       typecheck_type(symbol.type);

src/ansi-c/c_typecheck_base.h

@@ -61,7 +61,7 @@ class c_typecheck_baset:
   symbol_tablet &symbol_table;
   const irep_idt module;
   const irep_idt mode;
-  irep_idt current_symbol_id;
+  symbolt current_symbol;
 
   typedef std::unordered_map<irep_idt, typet, irep_id_hash> id_type_mapt;
   id_type_mapt parameter_map;

src/ansi-c/c_typecheck_type.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/simplify_expr.h>
 #include <util/arith_tools.h>
 #include <util/std_types.h>
@@ -551,9 +552,15 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
     {
       // not a constant and not infinity
 
-      assert(!current_symbol_id.empty());
+      PRECONDITION(!current_symbol.name.empty());
 
-      const symbolt &base_symbol=lookup(current_symbol_id);
+      if(current_symbol.is_static_lifetime)
+      {
+        error().source_location=current_symbol.location;
+        error() << "array size of static symbol `"
+                << current_symbol.base_name << "' is not constant" << eom;
+        throw 0;
+      }
 
       // Need to pull out! We insert new symbol.
       source_locationt source_location=size.find_source_location();
@@ -564,7 +571,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       do
       {
         suffix="$array_size"+std::to_string(count);
-        temp_identifier=id2string(base_symbol.name)+suffix;
+        temp_identifier=id2string(current_symbol.name)+suffix;
         count++;
       }
       while(symbol_table.symbols.find(temp_identifier)!=
@@ -573,13 +580,13 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       // add the symbol to symbol table
       auxiliary_symbolt new_symbol;
       new_symbol.name=temp_identifier;
-      new_symbol.pretty_name=id2string(base_symbol.pretty_name)+suffix;
-      new_symbol.base_name=id2string(base_symbol.base_name)+suffix;
+      new_symbol.pretty_name=id2string(current_symbol.pretty_name)+suffix;
+      new_symbol.base_name=id2string(current_symbol.base_name)+suffix;
       new_symbol.type=size.type();
       new_symbol.type.set(ID_C_constant, true);
       new_symbol.is_type=false;
       new_symbol.is_static_lifetime=false;
-      new_symbol.value.make_nil();
+      new_symbol.value=size;
       new_symbol.location=source_location;
 
       symbol_table.add(new_symbol);