C front-end: explicitly initialise nondet variables

This enables us to distinguish the case where the front-end intended a nondet
initialiser from an undefined variable, such as a "#return_value" global before
a call or on paths which throw an exception.

Author: smowton

src/linking/static_lifetime_init.cpp

@@ -53,14 +53,6 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
   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
@@ -77,14 +69,18 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
     return {}; // do not initialize
   }
 
-  if(symbol.value.id() == ID_nondet)
-  {
-    return {}; // do not initialize
-  }
-
   exprt rhs;
 
-  if(symbol.value.is_nil())
+  if((symbol.value.is_nil() && symbol.is_extern) ||
+     symbol.value.id() == ID_nondet)
+  {
+    // Nondet initialise if not linked, or if explicitly requested.
+    // Compilers would usually complain about the unlinked symbol case.
+    const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);
+    CHECK_RETURN(nondet.has_value());
+    rhs = *nondet;
+  }
+  else if(symbol.value.is_nil())
   {
     const auto zero = zero_initializer(symbol.type, symbol.location, ns);
     CHECK_RETURN(zero.has_value());