Mark some variables in Java with ID_C_no_nondet_initialization_allowed

This sets the flag to be true for __CPROVER_rounding_mode,
__CPROVER_malloc_object, java::@inflight_exception and static initializer proprietary variables

Author: svorenova

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -24,6 +24,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbol.base_name="__CPROVER_rounding_mode";
     symbol.name=CPROVER_PREFIX "rounding_mode";
     symbol.type=signed_int_type();
+    symbol.type.set(ID_C_no_nondet_initialization_allowed, true);
     symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
@@ -38,6 +39,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbol.base_name="__CPROVER_malloc_object";
     symbol.name=CPROVER_PREFIX "malloc_object";
     symbol.type=pointer_type(empty_typet());
+    symbol.type.set(ID_C_no_nondet_initialization_allowed, true);
     symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
@@ -51,6 +53,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_allowed, 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_allowed, true);
   new_symbol.value = value;
   new_symbol.is_lvalue = true;
   new_symbol.is_state_var = true;