Merge pull request #2643 from svorenova/fixup-nondet-static

Fix-up to nondet-static option [TG-4365]

Author: svorenova

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -51,6 +51,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME;
     symbol.mode = ID_java;
     symbol.type = pointer_type(empty_typet());
+    symbol.type.set(ID_C_no_nondet_initialization, true);
     symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
     symbol.is_file_local = false;
     symbol.is_static_lifetime = true;

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -91,6 +91,7 @@ static symbolt add_new_variable_symbol(
   new_symbol.pretty_name = name;
   new_symbol.base_name = name;
   new_symbol.type = type;
+  new_symbol.type.set(ID_C_no_nondet_initialization, true);
   new_symbol.value = value;
   new_symbol.is_lvalue = true;
   new_symbol.is_state_var = true;

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -84,6 +84,7 @@ symbol_exprt get_or_create_string_literal_symbol(
   symbolt new_symbol;
   new_symbol.name = escaped_symbol_name_with_prefix;
   new_symbol.type = string_type;
+  new_symbol.type.set(ID_C_constant, true);
   new_symbol.base_name = escaped_symbol_name;
   new_symbol.pretty_name = value;
   new_symbol.mode = ID_java;
@@ -131,6 +132,7 @@ symbol_exprt get_or_create_string_literal_symbol(
     array_symbol.is_state_var = true;
     array_symbol.value = data;
     array_symbol.type = array_symbol.value.type();
+    array_symbol.type.set(ID_C_constant, true);
 
     if(symbol_table.add(array_symbol))
       throw "failed to add constarray symbol to symbol table";
@@ -161,6 +163,7 @@ symbol_exprt get_or_create_string_literal_symbol(
       java_int_type(),
       symbol_table);
     return_symbol.type = return_symbol.value.type();
+    return_symbol.type.set(ID_C_constant, true);
     if(symbol_table.add(return_symbol))
       throw "failed to add return symbol to symbol table";
 

src/goto-instrument/nondet_static.cpp

@@ -42,6 +42,14 @@ void nondet_static(
       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))
+      {
+        continue;
+      }
+
       // static lifetime?
       if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
         continue;
@@ -50,11 +58,11 @@ void nondet_static(
       if(is_constant_or_has_constant_components(sym.type(), ns))
         continue;
 
-      i_it=init.insert_before(++i_it);
+      const goto_programt::instructiont original_instruction = instruction;
       i_it->make_assignment();
       i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
-      i_it->source_location=instruction.source_location;
-      i_it->function=instruction.function;
+      i_it->source_location = original_instruction.source_location;
+      i_it->function = original_instruction.function;
     }
     else if(instruction.is_function_call())
     {

src/util/irep_ids.def

@@ -665,6 +665,7 @@ IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
+IREP_ID_TWO(C_no_nondet_initialization, #no_nondet_initialization)
 IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
 IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
 IREP_ID_TWO(ignored_method, java::com.diffblue.IgnoredMethodImplementation)