Pull out a function to check conditions for nondet-static

So that the function can be called from other files too

Author: svorenova

src/goto-instrument/nondet_static.cpp

@@ -18,6 +18,39 @@ Date: November 2011
 
 #include <linking/static_lifetime_init.h>
 
+/// See the return.
+/// \param sym The symbol expression to analyze.
+/// \param ns Namespace for resolving type information
+/// \return True if the symbol expression holds a static symbol which can be
+/// nondeterministically initialized, false otherwise.
+bool is_nondet_initializable_static(
+  const symbol_exprt &sym,
+  const namespacet &ns)
+{
+  const irep_idt &id = sym.get_identifier();
+
+  // is it a __CPROVER_* variable?
+  if(has_prefix(id2string(id), CPROVER_PREFIX))
+    return false;
+
+  // variable not in symbol table such as symex variable?
+  if(!ns.get_symbol_table().has_symbol(id))
+    return false;
+
+  // is the type explicitly marked as not to be nondet initialized?
+  if(ns.lookup(id).type.get_bool(ID_C_no_nondet_initialization))
+    return false;
+
+  // static lifetime?
+  if(!ns.lookup(id).is_static_lifetime)
+    return false;
+
+  // constant?
+  return !is_constant_or_has_constant_components(sym.type(), ns) &&
+         !is_constant_or_has_constant_components(ns.lookup(id).type, ns);
+}
+
+
 void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions,
@@ -38,34 +71,17 @@ void nondet_static(
       const symbol_exprt &sym=to_symbol_expr(
           to_code_assign(instruction.code).lhs());
 
-      // is it a __CPROVER_* variable?
-      if(has_prefix(id2string(sym.get_identifier()), CPROVER_PREFIX))
-        continue;
-
-      // any other internal variable such as Java specific?
-      if(
-        ns.lookup(sym.get_identifier())
-          .type.get_bool(ID_C_no_nondet_initialization))
+      if(is_nondet_initializable_static(sym, ns))
       {
-        continue;
+        const goto_programt::instructiont original_instruction = instruction;
+        i_it->make_assignment();
+        i_it->code = code_assignt(
+          sym,
+          side_effect_expr_nondett(
+            sym.type(), original_instruction.source_location));
+        i_it->source_location = original_instruction.source_location;
+        i_it->function = original_instruction.function;
       }
-
-      // static lifetime?
-      if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
-        continue;
-
-      // constant?
-      if(is_constant_or_has_constant_components(sym.type(), ns))
-        continue;
-
-      const goto_programt::instructiont original_instruction = instruction;
-      i_it->make_assignment();
-      i_it->code = code_assignt(
-        sym,
-        side_effect_expr_nondett(
-          sym.type(), original_instruction.source_location));
-      i_it->source_location = original_instruction.source_location;
-      i_it->function = original_instruction.function;
     }
     else if(instruction.is_function_call())
     {

src/goto-instrument/nondet_static.h

@@ -18,6 +18,11 @@ Date: November 2011
 class goto_modelt;
 class namespacet;
 class goto_functionst;
+class symbol_exprt;
+
+bool is_nondet_initializable_static(
+  const symbol_exprt &sym,
+  const namespacet &ns);
 
 void nondet_static(
   const namespacet &ns,