Merge pull request #1156 from smowton/smowton/fix/global_variable_nondet_init

Fix nondet static field initialisation

Author: smowton

regression/cbmc-java/external_getstatic1/test.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/external_getstatic1/test.desc

@@ -0,0 +1,16 @@
+class A
+{
+  public static A external_global;
+  public int i;
+};
+
+public class test
+{
+  public static void main()
+  {
+    if(A.external_global == null)
+      return;
+    A local = A.external_global;
+    assert(local instanceof A);
+  }
+}

regression/cbmc-java/external_getstatic1/test.java

@@ -85,7 +85,7 @@ static goto_programt::targett insert_nondet_init_code(
     symbol_table,
     source_loc,
     true,
-    true,
+    allocation_typet::DYNAMIC,
     !nullable,
     max_nondet_array_length,
     update_in_placet::NO_UPDATE_IN_PLACE);

src/goto-programs/convert_nondet.cpp

@@ -2014,6 +2014,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const bool is_assertions_disabled_field=
         field_name.find("$assertionsDisabled")!=std::string::npos;
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
+
+      // If external, create a symbol table entry for this static field:
+      check_static_field_stub(symbol_expr, field_name);
+
       if(lazy_methods)
       {
         if(arg0.type().id()==ID_symbol)
@@ -2056,6 +2060,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
+
+      // If external, create a symbol table entry for this static field:
+      check_static_field_stub(symbol_expr, field_name);
+
       if(lazy_methods && arg0.type().id()==ID_symbol)
       {
         lazy_methods->add_needed_class(

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -113,6 +113,7 @@ codet java_bytecode_instrumentt::throw_exception(
       false,
       symbol_table,
       max_array_length,
+      allocation_typet::LOCAL,
       original_loc);
   }
   else

src/java_bytecode/java_bytecode_instrument.cpp

@@ -118,6 +118,7 @@ void java_static_lifetime_init(
           allow_null,
           symbol_table,
           max_nondet_array_length,
+          allocation_typet::GLOBAL,
           source_location);
         code_assignt assignment(sym.symbol_expr(), newsym);
         code_block.add(assignment);
@@ -180,6 +181,7 @@ exprt::operandst java_build_arguments(
         allow_null,
         symbol_table,
         max_nondet_array_length,
+        allocation_typet::LOCAL,
         function.location);
 
     // record as an input