Static-lifetime symbols require compile-time constant initialisers

regression/ansi-c/static4/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int y = 42;
+  static int x = y;
+
+  __CPROVER_assert(x == 42, "local static");
+}

regression/ansi-c/static4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+expected constant expression
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_code.cpp

@@ -308,12 +308,19 @@ void c_typecheck_baset::typecheck_decl(codet &code)
     // see if it's a typedef
     // or a function
     // or static
-    if(symbol.is_type ||
-       symbol.type.id()==ID_code ||
-       symbol.is_static_lifetime)
+    if(symbol.is_type || symbol.type.id() == ID_code)
     {
       // we ignore
     }
+    else if(symbol.is_static_lifetime)
+    {
+      // make sure the initialization value is a compile-time constant
+      if(symbol.value.is_not_nil())
+      {
+        exprt init_value = symbol.value;
+        make_constant(init_value);
+      }
+    }
     else
     {
       code_frontend_declt decl(symbol.symbol_expr());

src/ansi-c/c_typecheck_expr.cpp

@@ -3925,6 +3925,38 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
   throw 0;
 }
 
+class is_compile_time_constantt : public is_constantt
+{
+public:
+  explicit is_compile_time_constantt(const namespacet &ns) : ns(ns)
+  {
+  }
+
+protected:
+  const namespacet &ns;
+
+  bool is_constant(const exprt &e) const override
+  {
+    if(e.id() == ID_infinity)
+      return true;
+    else
+      return is_constantt::is_constant(e);
+  }
+
+  bool is_constant_address_of(const exprt &e) const override
+  {
+    if(e.id() == ID_symbol)
+    {
+      return e.type().id() == ID_code ||
+             ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
+    }
+    else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
+      return true;
+    else
+      return is_constantt::is_constant_address_of(e);
+  }
+};
+
 void c_typecheck_baset::make_constant(exprt &expr)
 {
   // Floating-point expressions may require a rounding mode.
@@ -3936,8 +3968,7 @@ void c_typecheck_baset::make_constant(exprt &expr)
 
   simplify(expr, *this);
 
-  if(!expr.is_constant() &&
-     expr.id()!=ID_infinity)
+  if(!is_compile_time_constantt(*this)(expr))
   {
     error().source_location=expr.find_source_location();
     error() << "expected constant expression, but got '" << to_string(expr)
@@ -3952,8 +3983,7 @@ void c_typecheck_baset::make_constant_index(exprt &expr)
   make_index_type(expr);
   simplify(expr, *this);
 
-  if(!expr.is_constant() &&
-     expr.id()!=ID_infinity)
+  if(!is_compile_time_constantt(*this)(expr))
   {
     error().source_location=expr.find_source_location();
     error() << "conversion to integer constant failed" << eom;

src/util/expr_util.cpp

@@ -236,6 +236,7 @@ bool is_constantt::is_constant(const exprt &expr) const
     expr.id() == ID_typecast || expr.id() == ID_array_of ||
     expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
     expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
+    expr.id() == ID_empty_union ||
     // byte_update works, byte_extract may be out-of-bounds
     expr.id() == ID_byte_update_big_endian ||
     expr.id() == ID_byte_update_little_endian)