Static-lifetime symbols require compile-time constant initialisers

We previously silently accepted initialisers that weren't compile-time
constants, resulting in surprising behaviour: the assertion in the
enclosed regression test would fail, because x ended up being
initialised before y.

Author: tautschnig

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());