Initialization ordering

regression/cbmc/Float-rounding/compile_time_rounding.desc

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

src/linking/static_lifetime_init.cpp

@@ -22,6 +22,83 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_functions.h>
 
+static optionalt<codet>
+static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
+{
+  const namespacet ns(symbol_table);
+  const symbolt &symbol = ns.lookup(identifier);
+
+  if(!symbol.is_static_lifetime)
+    return {};
+
+  if(symbol.is_type || symbol.is_macro)
+    return {};
+
+  // special values
+  if(
+    identifier == CPROVER_PREFIX "constant_infinity_uint" ||
+    identifier == CPROVER_PREFIX "memory" || identifier == "__func__" ||
+    identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__" ||
+    identifier == "argc'" || identifier == "argv'" || identifier == "envp'" ||
+    identifier == "envp_size'")
+    return {};
+
+  // just for linking
+  if(has_prefix(id2string(identifier), CPROVER_PREFIX "architecture_"))
+    return {};
+
+  const typet &type = ns.follow(symbol.type);
+
+  // check type
+  if(type.id() == ID_code || type.id() == ID_empty)
+    return {};
+
+  // We won't try to initialize any symbols that have
+  // remained incomplete.
+
+  if(symbol.value.is_nil() && symbol.is_extern)
+    // Compilers would usually complain about these
+    // symbols being undefined.
+    return {};
+
+  if(type.id() == ID_array && to_array_type(type).size().is_nil())
+  {
+    // C standard 6.9.2, paragraph 5
+    // adjust the type to an array of size 1
+    symbolt &writable_symbol = *symbol_table.get_writeable(identifier);
+    writable_symbol.type = type;
+    writable_symbol.type.set(ID_size, from_integer(1, size_type()));
+  }
+
+  if(
+    (type.id() == ID_struct || type.id() == ID_union) &&
+    to_struct_union_type(type).is_incomplete())
+  {
+    return {}; // do not initialize
+  }
+
+  if(symbol.value.id() == ID_nondet)
+  {
+    return {}; // do not initialize
+  }
+
+  exprt rhs;
+
+  if(symbol.value.is_nil())
+  {
+    const auto zero = zero_initializer(symbol.type, symbol.location, ns);
+    CHECK_RETURN(zero.has_value());
+    rhs = *zero;
+  }
+  else
+    rhs = symbol.value;
+
+  code_assignt code(symbol.symbol_expr(), rhs);
+  code.add_source_location() = symbol.location;
+
+  return std::move(code);
+}
+
 void static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location)
@@ -50,86 +127,25 @@ void static_lifetime_init(
     symbols.insert(id2string(symbol_pair.first));
   }
 
+  // first do framework variables
   for(const std::string &id : symbols)
-  {
-    const symbolt &symbol=ns.lookup(id);
-
-    const irep_idt &identifier=symbol.name;
-
-    if(!symbol.is_static_lifetime)
-      continue;
-
-    if(symbol.is_type || symbol.is_macro)
-      continue;
-
-    // special values
-    if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||
-       identifier==CPROVER_PREFIX "memory" ||
-       identifier=="__func__" ||
-       identifier=="__FUNCTION__" ||
-       identifier=="__PRETTY_FUNCTION__" ||
-       identifier=="argc'" ||
-       identifier=="argv'" ||
-       identifier=="envp'" ||
-       identifier=="envp_size'")
-      continue;
-
-    // just for linking
-    if(has_prefix(id, CPROVER_PREFIX "architecture_"))
-      continue;
-
-    const typet &type=ns.follow(symbol.type);
-
-    // check type
-    if(type.id()==ID_code ||
-       type.id()==ID_empty)
-      continue;
-
-    // We won't try to initialize any symbols that have
-    // remained incomplete.
-
-    if(symbol.value.is_nil() &&
-       symbol.is_extern)
-      // Compilers would usually complain about these
-      // symbols being undefined.
-      continue;
-
-    if(type.id()==ID_array &&
-       to_array_type(type).size().is_nil())
+    if(has_prefix(id, CPROVER_PREFIX))
     {
-      // C standard 6.9.2, paragraph 5
-      // adjust the type to an array of size 1
-      symbolt &writable_symbol = *symbol_table.get_writeable(identifier);
-      writable_symbol.type = type;
-      writable_symbol.type.set(ID_size, from_integer(1, size_type()));
+      auto code = static_lifetime_init(id, symbol_table);
+      if(code.has_value())
+        dest.add(std::move(*code));
     }
 
-    if(
-      (type.id() == ID_struct || type.id() == ID_union) &&
-      to_struct_union_type(type).is_incomplete())
-      continue; // do not initialize
-
-    if(symbol.value.id()==ID_nondet)
-      continue; // do not initialize
-
-    exprt rhs;
-
-    if(symbol.value.is_nil())
+  // now all other variables
+  for(const std::string &id : symbols)
+    if(!has_prefix(id, CPROVER_PREFIX))
     {
-      const auto zero = zero_initializer(symbol.type, symbol.location, ns);
-      CHECK_RETURN(zero.has_value());
-      rhs = *zero;
+      auto code = static_lifetime_init(id, symbol_table);
+      if(code.has_value())
+        dest.add(std::move(*code));
     }
-    else
-      rhs=symbol.value;
-
-    code_assignt code(symbol.symbol_expr(), rhs);
-    code.add_source_location()=symbol.location;
-
-    dest.add(code);
-  }
 
-  // call designated "initialization" functions
+  // now call designated "initialization" functions
 
   for(const std::string &id : symbols)
   {