From 655978c03726fa977d8f0f2320227f573c24b88f Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Mon, 30 Jul 2018 16:02:30 +0100
Subject: [PATCH 1/8] Record nondet-static option in java_bytecode_language

---
 jbmc/src/java_bytecode/java_bytecode_language.cpp | 2 ++
 jbmc/src/java_bytecode/java_bytecode_language.h   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 8499e5913e6..335633fea76 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -157,6 +157,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     java_cp_include_files=".*";
 
+  nondet_static = cmd.isset("nondet-static");
+
   language_options_initialized=true;
 }
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index 20885ed689c..387ac57db04 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -192,6 +192,7 @@ class java_bytecode_languaget:public languaget
   bool throw_assertion_error;
   java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;
+  bool nondet_static;
 
   // list of classes to force load even without reference from the entry point
   std::vector<irep_idt> java_load_classes;

From 5fe44edd7c79c64672527853873c0e1189dd6fe2 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Mon, 30 Jul 2018 16:08:23 +0100
Subject: [PATCH 2/8] Pass information to clinit_wrapper constructors

Pass parameters necessary to nondet-initialize variables
---
 .../java_bytecode/java_bytecode_language.cpp  | 13 +++-
 .../java_static_initializers.cpp              | 59 +++++++++++++++----
 .../java_bytecode/java_static_initializers.h  | 10 +++-
 3 files changed, 68 insertions(+), 14 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 335633fea76..c08a914bd88 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -1031,9 +1031,18 @@ bool java_bytecode_languaget::convert_single_method(
     case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
       if(threading_support)
         symbol.value = get_thread_safe_clinit_wrapper_body(
-          function_id, symbol_table);
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       else
-        symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
+        symbol.value = get_clinit_wrapper_body(
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       symbol.value =
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index b4daf706820..4dfe102d9fe 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -184,10 +184,19 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 /// \param symbol_table: symbol table
 /// \param class_name: name of the class to generate clinit wrapper calls for
 /// \param [out] init_body: appended with calls to clinit wrapper
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
 static void clinit_wrapper_do_recursive_calls(
   const symbol_tablet &symbol_table,
   const irep_idt &class_name,
-  code_blockt &init_body)
+  code_blockt &init_body,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
   for(const auto &base : to_class_type(class_symbol.type).bases())
@@ -316,9 +325,9 @@ static void create_clinit_wrapper_symbols(
     "clinit wrapper");
 }
 
-/// Thread safe version of the static initialiser.
+/// Thread safe version of the static initializer.
 ///
-/// Produces the static initialiser wrapper body for the given function. This
+/// Produces the static initializer wrapper body for the given function. This
 /// static initializer implements (a simplification of) the algorithm defined
 /// in Section 5.5 of the JVM Specs. This function, or wrapper, checks whether
 /// static init has already taken place, calls the actual `<clinit>` method if
@@ -382,10 +391,19 @@ static void create_clinit_wrapper_symbols(
 /// \param function_id: clinit wrapper function id (the wrapper_method_symbol
 ///   name created by `create_clinit_wrapper_symbols`)
 /// \param symbol_table: global symbol table
-/// \return the body of the static initialiser wrapper
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
+/// \return the body of the static initializer wrapper
 codet get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
   irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
@@ -536,7 +554,13 @@ codet get_thread_safe_clinit_wrapper_body(
   //
   {
     code_blockt init_body;
-    clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
+    clinit_wrapper_do_recursive_calls(
+      symbol_table,
+      class_name,
+      init_body,
+      nondet_static,
+      object_factory_parameters,
+      pointer_type_selector);
     function_body.append(init_body);
   }
 
@@ -557,15 +581,24 @@ codet get_thread_safe_clinit_wrapper_body(
   return function_body;
 }
 
-/// Produces the static initialiser wrapper body for the given function.
+/// Produces the static initializer wrapper body for the given function.
 /// Note: this version of the clinit wrapper is not thread safe.
 /// \param function_id: clinit wrapper function id (the wrapper_method_symbol
 ///   name created by `create_clinit_wrapper_symbols`)
 /// \param symbol_table: global symbol table
-/// \return the body of the static initialiser wrapper/
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
+/// \return the body of the static initializer wrapper
 codet get_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   // Assume that class C extends class C' and implements interfaces
   // I1, ..., In. We now create the following function (possibly recursively
@@ -609,7 +642,13 @@ codet get_clinit_wrapper_body(
   code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
   init_body.move_to_operands(set_already_run);
 
-  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
+  clinit_wrapper_do_recursive_calls(
+    symbol_table,
+    class_name,
+    init_body,
+    nondet_static,
+    object_factory_parameters,
+    pointer_type_selector);
 
   wrapper_body.then_case() = init_body;
 
diff --git a/jbmc/src/java_bytecode/java_static_initializers.h b/jbmc/src/java_bytecode/java_static_initializers.h
index f8daab5b0cd..471ce646a2a 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.h
+++ b/jbmc/src/java_bytecode/java_static_initializers.h
@@ -29,11 +29,17 @@ void create_static_initializer_wrappers(
 
 codet get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
 
 codet get_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
 
 class stub_global_initializer_factoryt
 {

From 48797b0993b608328680e575f8ebc53f18c92051 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Thu, 2 Aug 2018 11:16:43 +0100
Subject: [PATCH 3/8] Nondet-initialize variables in clinit_wrapper constructor

If nondet-static option is used
---
 .../java_static_initializers.cpp              | 61 +++++++++++++++++--
 1 file changed, 56 insertions(+), 5 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index 4dfe102d9fe..dda21f4c971 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -180,7 +180,9 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 
 /// Generates codet that iterates through the base types of the class specified
 /// by class_name, C, and recursively adds calls to their clinit wrapper.
-/// Finally a call to the clinint wrapper of C is made.
+/// Finally a call to the clinit of C is made. If nondet-static option was
+/// given then all static variables that are not constants (i.e. final) are
+/// then re-assigned to a nondet value.
 /// \param symbol_table: symbol table
 /// \param class_name: name of the class to generate clinit wrapper calls for
 /// \param [out] init_body: appended with calls to clinit wrapper
@@ -191,7 +193,7 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields (only needed if nondet-static is true)
 static void clinit_wrapper_do_recursive_calls(
-  const symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const irep_idt &class_name,
   code_blockt &init_body,
   const bool nondet_static,
@@ -218,6 +220,52 @@ static void clinit_wrapper_do_recursive_calls(
     code_function_callt call_real_init;
     call_real_init.function() = find_sym_it->second.symbol_expr();
     init_body.move_to_operands(call_real_init);
+
+    // Add a standard nondet initialization for each non-final static field
+    // of this class. Note this is the same invocation used in
+    // get_stub_initializer_body and java_static_lifetime_init.
+    if(nondet_static)
+    {
+      object_factory_parameterst parameters = object_factory_parameters;
+      parameters.function_id = clinit_wrapper_name(class_name);
+
+      std::vector<irep_idt> nondet_ids;
+      std::for_each(
+        symbol_table.symbols.begin(),
+        symbol_table.symbols.end(),
+        [&](const std::pair<irep_idt, symbolt> &symbol) {
+          if(
+            symbol.second.type.get(ID_C_class) == class_name &&
+            symbol.second.is_static_lifetime &&
+            !symbol.second.type.get_bool(ID_C_constant))
+          {
+            nondet_ids.push_back(symbol.first);
+          }
+        });
+
+      for(const auto &id : nondet_ids)
+      {
+        const symbol_exprt new_global_symbol =
+          symbol_table.lookup_ref(id).symbol_expr();
+
+        parameters.max_nonnull_tree_depth =
+          is_non_null_library_global(id)
+            ? std::max(
+                size_t(1), object_factory_parameters.max_nonnull_tree_depth)
+            : object_factory_parameters.max_nonnull_tree_depth;
+
+        gen_nondet_init(
+          new_global_symbol,
+          init_body,
+          symbol_table,
+          source_locationt(),
+          false,
+          allocation_typet::DYNAMIC,
+          parameters,
+          pointer_type_selector,
+          update_in_placet::NO_UPDATE_IN_PLACE);
+      }
+    }
   }
 }
 
@@ -374,7 +422,8 @@ static void create_clinit_wrapper_symbols(
 ///   // ...
 ///   java::In::clinit_wrapper();
 ///
-///   java::C::<clinit>();
+///   java::C::<clinit>();  // or nondet-initialization of all static
+///                         // variables of C if nondet-static is true
 ///
 ///   // Setting this variable to INIT_COMPLETE will let other threads "cross"
 ///   // beyond the assume() statement above in this function.
@@ -550,7 +599,8 @@ codet get_thread_safe_clinit_wrapper_body(
   //  // ...
   //  java::In::clinit_wrapper();
   //
-  //  java::C::<clinit>();
+  //  java::C::<clinit>(); // or nondet-initialization of all static
+  //                       // variables of C if nondet-static is true
   //
   {
     code_blockt init_body;
@@ -616,7 +666,8 @@ codet get_clinit_wrapper_body(
   //     // ...
   //     java::In::clinit_wrapper();
   //
-  //     java::C::<clinit>();
+  //     java::C::<clinit>(); // or nondet-initialization of all static
+  //                          // variables of C if nondet-static is true
   //   }
   // }
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);

From 9e6caba19a59dcd29c153152e982c2a688b3a37e Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Mon, 6 Aug 2018 13:57:45 +0100
Subject: [PATCH 4/8] Mark final fields in Java as constants

This will also make sure that they won't get nondet-initialized with
nondet-static option
---
 jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index e92d1906167..46beec8965b 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -645,6 +645,7 @@ void java_bytecode_convert_classt::convert(
     // link matches the method used by java_bytecode_convert_method::convert
     // for methods.
     new_symbol.type.set(ID_C_class, class_symbol.name);
+    new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
       "."+id2string(f.name);
     new_symbol.mode=ID_java;

From 2ecf8e8ea6e0ee51d7c061a933054788796d1516 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Mon, 6 Aug 2018 11:31:05 +0100
Subject: [PATCH 5/8] Add nondet-static option to JBMC

The option already appears in process_goto_functions before, the flag just needed to be read.
---
 jbmc/src/jbmc/jbmc_parse_options.cpp | 7 +++++++
 jbmc/src/jbmc/jbmc_parse_options.h   | 1 +
 2 files changed, 8 insertions(+)

diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index cdcb16b6062..abcfc87057b 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -124,6 +124,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 
+  if(cmdline.isset("nondet-static"))
+    options.set_option("nondet-static", true);
+
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
@@ -1095,6 +1098,10 @@ void jbmc_parse_optionst::help()
     "                              will be restricted to loaded methods in this case,\n" // NOLINT(*)
     "                              and only output after the symex phase.\n"
     "\n"
+    "Semantic transformations:\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
+    "\n"
     "BMC options:\n"
     HELP_BMC
     "\n"
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index b4fab93735c..d0c5ad3d094 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -67,6 +67,7 @@ class optionst;
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(verbosity):" \
+  "(nondet-static)" \
   "(version)" \
   "(cover):(symex-coverage-report):" \
   OPT_TIMESTAMP \

From 46d47e076528c201a6c66d1e316d84e2f31bd475 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Mon, 6 Aug 2018 11:44:07 +0100
Subject: [PATCH 6/8] Add a regression test for nondet-static

---
 .../jbmc/nondet-static/My$PInner.class        | Bin 0 -> 422 bytes
 .../jbmc/nondet-static/My$PSInner.class       | Bin 0 -> 1480 bytes
 .../jbmc/nondet-static/My$PrInner.class       | Bin 0 -> 415 bytes
 .../jbmc/nondet-static/My$PrSInner.class      | Bin 0 -> 1433 bytes
 jbmc/regression/jbmc/nondet-static/My.class   | Bin 0 -> 3011 bytes
 jbmc/regression/jbmc/nondet-static/My.java    | 238 ++++++++++++++++++
 jbmc/regression/jbmc/nondet-static/test.desc  |  70 ++++++
 7 files changed, 308 insertions(+)
 create mode 100644 jbmc/regression/jbmc/nondet-static/My$PInner.class
 create mode 100644 jbmc/regression/jbmc/nondet-static/My$PSInner.class
 create mode 100644 jbmc/regression/jbmc/nondet-static/My$PrInner.class
 create mode 100644 jbmc/regression/jbmc/nondet-static/My$PrSInner.class
 create mode 100644 jbmc/regression/jbmc/nondet-static/My.class
 create mode 100644 jbmc/regression/jbmc/nondet-static/My.java
 create mode 100644 jbmc/regression/jbmc/nondet-static/test.desc

diff --git a/jbmc/regression/jbmc/nondet-static/My$PInner.class b/jbmc/regression/jbmc/nondet-static/My$PInner.class
new file mode 100644
index 0000000000000000000000000000000000000000..58d8d6f41f8bfd155d9d062995bd5d4abd4d2c5d
GIT binary patch
literal 422
zcmYjN%SyvQ6g`u~#-^!_^<7^GUDOIz!JX1gK`68;DBVx%s3~z$l2qttxe&pHAK*uc
zXHpRvxWhT;-g6&c-yfd<&ahX6jSUYDHeJ+QYzx?vhf@L36)1ONon}&J0~t+~%>p6d
zOcJ9PvZpYupAh%@vvcB$P={Gtz-<`fa6qLK-z$MiFVyO4`aD$0og7AFs=at5qk&99
zgMUfK7}DpatF=l5{QU1kGEEiv5?$+ajorN4c$$pVWoYc&{_J=xU!)HYB_BR^T<i)I
z{|W>GqqicdA6wVMu^MGuvteem`ZFBx1P+(8v4sT`Ku01Ai>RUa9|wWyV9vnjqs+KO
y)Ml>5-)kPdK{VfCz2@~5M&kzTBVb&gXJHwuM9k0KI0M#*Eb1#c%h@<d72*dSQbp(h

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/nondet-static/My$PSInner.class b/jbmc/regression/jbmc/nondet-static/My$PSInner.class
new file mode 100644
index 0000000000000000000000000000000000000000..f3432fcb033aa8d0b33ca6c71708db361d65b5bd
GIT binary patch
literal 1480
zcmZux*-{fh6g{17k~r*O1i=l^1eGN~K!~_R!AQa)7)8s6A&wX-PEwOV6`y344{9E;
zw8{_gqb$#Dz@&<KIj8UGb9=dWdj9<V`5V9t-bT=i#{wCFCjw6emIYP>o(W{5=)-dv
ztqSC#$YV`L>jpNWXvd}mF9fy(wgp}qC>VI9;Hyq4sH_Z<0@DIB0<#J|xqa)<nkZY&
z-bB`^+k3XVsNk=DU`|`6;?(MvQ!iNM1KZCdD?P<kXy7tLuH&z|G!wP%YTZ52xj~@n
z%34C47otIkj!?Sfl<G@NjwcFKGnMzYLPxIT*lP!$c5Qdt+AUM*&Q*$5xnQ{^iBH8q
z{bQ-7U~Ft<9mjSROwF0HRjb*YFmw5%k<&?DDQXpqcC9utIXS8KV?EBKDUr^CWNR?p
z8q7%07f*Or>@0n@H6zs;%t;VV7t5!2j&4;B+@if)k{cTNqj713iQ5=7F@~6lgupEc
zZ^~#?U_@Y8;12GZxFn-~#0<PPv4fO}0mKx#&h=FMZ%ka4)vig>b%7fg<i(q1Qs``E
zuJ7*K#X3Ke{1FRwXqDNZcs5aBYA-)Wpc@ffM2w?|97HqEqM66g%nix?7-Fn&g<~JC
zGUgey&SPliNyt&Tnr7ZpGcT=~70}FbkOvTF++1%!YNd4+PBW{h{YvUY=QyJYvLXk^
zjuH9BfsYap(&8v4IW|uWnBwC^XBe|cQIX_9Jp%;3Bm9N2YR#o{&dX_dIp@8cAus1W
zFK5upxq!v<=L~%HIA_{xO~2Qg_r07xFXxii?&{p`2;;&3W_*VHPk?uU2BN_RF8qMm
zK-(|0?}U%h(Lg7~E-iM8XlSvAZi5pcJrQiW0~GyQ^flc|ntalz1^y(##}wd~66W)2
y=R50X3y0YDVYYjm4NvmIDK;{Vd8`muaUYvl;%D-ZxjsC?G&#x@d-?xOBJvNi2+P9&

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/nondet-static/My$PrInner.class b/jbmc/regression/jbmc/nondet-static/My$PrInner.class
new file mode 100644
index 0000000000000000000000000000000000000000..54c96ed1500ee5e6d878b4140641d9768d1622ce
GIT binary patch
literal 415
zcmYjNO-sW-5Ph4(#>TCU^}BxHp@&+*D)goZ5)cZB3QF#qx@t<?lza&JSsq02;1BRe
ziL;@gmzjO@=DpdO@1M^v03+--VPeyPg)JLh8#@f<?D3R=jTu^As`5gpA{0p}O%gB$
zYnExgQ9Q?a?}V@)RA+?GV-*({40c}^4ntzR^g%MT{aDHC@+Fely@(R3bo_K8l2Bx^
z#`B`34M~2Rjg^ua1Fy4}h&-1>aI)>qNt)-}rDZmeSFtv<gX(xHUImAPB@T{V8++9A
zr(ke(!!Qx*X?PP&<)olZ`}&(kP~m{CV9|aiwy}T)$dZtOMRd{pk6l-f(3c>VqeXd{
u(1?&h*%=(YgAG1lyw&<PMePP$!llUTw}Ta|)%<!LH?T_CAx_Wl!1x6kq(?6R

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/nondet-static/My$PrSInner.class b/jbmc/regression/jbmc/nondet-static/My$PrSInner.class
new file mode 100644
index 0000000000000000000000000000000000000000..2c9413cd7c34cebf2114120d3869bae6e47ad5b3
GIT binary patch
literal 1433
zcmZuxX-^YT6g|^Uw_(bT6~rC2MTJrpSt>3lSZ&#gRY+WhI$}wkHq%1FPcrd?+7B2_
z`~m(b<GGKe5a!D{cRBCA`|f))fB*gZ17Hjr5p?5`z+-_qfhPh_1?B}74D{fcSQ&xm
z23{a5RxX4^15qrAvn;S8uqu!jSPS802n7wk>WBs{BSuPKRA5YCTtioO+uF5;%a*e>
zoN?;*mhH}H@K--_O?0l})asT~FIeRr+s~FYm0}eNScb?t{;EqcQN>*qcMsy+K(D$|
zONe<P3WTT#rb|w#KFh`N1RK@oDj#eOZP}7zFYbKawB0ppv&=|mwo<gp1<Ngoe;Cy3
zpGq|i;bk|UaU9##U@D#~TeX_aOf;L@8#v1HP=-}3+O^uiWHPCC<V21_Qxa-9%#S2b
zd2~<YQsVW*6P{x`t}uFP&6s%Mbg_JRS|eZCaf|kRNzN9^?G4Elm>5LNL_**e`c2#v
z>xRI9z;%H;xNG9PSiOja@XEw%Oql3HOhd<+ixmC3i3?KgiY&S+a82CX=;xtM%tu3e
zbN$lhwq30Ah2-`)sa>ngyNPEK1y<?ia|AjO!8yceMWh|Y>_{=2QOs@0y|_qU!zJ22
zT&B-XRGiHyW<O*@4yc%?Rm`I+<{T7rDC9oG={M{3$;4Eg<5SF|kt5uV)1q>S-Y{7s
z2L|^M{!YWk5D-+s1te*k2Lg=nyF_~!<CtJX7Wb<Rp#MPVD}C+cS}N~(DT7|hNiSu<
zOF8AG)V-9`m^s_0|C>jjX|I|-ubTJ0l-e03!k9fC@fXMs0(hf05D7G3{6tFw=5IvT
z!~1A$ppC(H73`2;NCi8o4l)r?3B9TIGw4%6t*P#kt2-F~G+JqAp!0tiMwVWVZ)=6G
rZIv%6&x<P{C0_^Dk;VoV@RrJVRJ`ZqKj2y)9%7ViuwplJDH#6&U?9r@

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/nondet-static/My.class b/jbmc/regression/jbmc/nondet-static/My.class
new file mode 100644
index 0000000000000000000000000000000000000000..df0cb67c70161275baec59bf5c94bb3bf894336d
GIT binary patch
literal 3011
zcma)8X;f5Y7=GSwfXfVn;wXx!xl*{~f*XoknHC9(Vw#%T03!~J0}ca9D(>Z4X{orE
zil(^aaMGKeqd(FX^+#Eqv_(57+m805e)-FK-^+5ppdTIadB1nL&->l`KJ(ps?a_rx
z0EXa<fkg&_21*Q+8d&VYXoO->=0r5Y0_6e~0!svz3RJp~fmZ~UiMw22g+P_SN`X}Z
zs|D5wtQA-%uwLL*Cmh1;5N3xkJA~PRN&)6`2%iI0E{4|xHVAAK*d(x7V2i+3f!CcN
z;UnQA;UnQA;UnQA;UnQAydm(Wz&3&H0&fYtEwIDI``c+?m)u^pf!&1IoKS9NFz5>r
z+?E|5@RpVN$_PeIs3BqGG?v8VG=x;?AOd9)RB4*PV1Xe5LkVrOio6xx0ReBYa6o1-
z>?`zzG6;^+1$<5X_>y2**c%Mb@CM3#4xSTPDQ4jUreS0rM`?(Q8LfE8iihgs+#sqn
zBwS)RFNO=ma7FY2zb{b0*H(A~jH$hOlTqVK3VejtS^l7Ja`~b>Uue2FFTjzQQU0Jm
zJccV$Gkeb<c(O|Jy@46tkYDl*MN#2}{xUAf%C6+wAV2?S*Q4EJZaCx*7IHE^H|)(X
z&i0mCm$Kvx?BQoTDnHQBhxfy6T)8FXp?u#&zwE)tuIw+*ix8Jx*~=b>%kmnYx8*cW
z!6})>L1b6DF%Lz2t9b#h8?*3?8{-8g2uu`sR^T~gy0I7g+}Mu;Ze&YrvcMEc<j88O
zz%+qef$5T%A*-1JFN%8*bKH1G;9Y@30*7(LjT%`U6*wmDd$Kw%a6+I~;G`r@$?CMg
zY|J6FX`vLkoB4zUJ254%$d@1fSE&Ah^Rwe2m;0tHAhhQJY7?<#7vo!8?hWw35>vH&
zJ!eMm**pwye!j1)tk=MS18rxJ?xg9?VBHxaPGahRcWxves$VfocZTauy6%h+C$3><
zycylI_STfMHrM1?yKC}zd+5$T`O*9{YYV67f>%zFhGkhDmSurhmNmk*Bc5lUFp1X+
zS?se|tT^k%vMd?4E>VqTSvZzu?O2xOV_8-Z+hn}JzRi~`qO#(wE6cL9*pi5st%G;S
z;$Z(JD@%;LlbDl?gt?3{Y-MjGTB)y#`iXr$PSo{2=Mm#Evio%U0I?A`cf;8yAz-at
zQ3q`&E?RTkF`5$}YogUTwBBPEC+Nj(^kR?EqPVTrvYp;CQD<qdvvg?LGD$D)s23-<
zY}rX`*;#MdMQ3?TXX)CqWjDRJyI$O*c}o*Ln_8OaWw$huVzZcd+-5QHMDvy=QuX5A
zdU2oTEhFgL)G~s8cFPE!v{@qPZ?i-&pn1y(2I|Fw^y0MUElmt=YH4DK-O|KRo5jR1
zo5jTN<}FR6>%}AV;ud$=&tudy>h3Iy+#!OeJy^i&0z|<FgV$~p!h?lKf*)N`gcKB`
z9|B0jB8)%~V^P9C+)_Tw!~CNv$9z=qRZF;HDJuEjN-V>AEXQW7z;;xjnj;6Xicj&?
zd`z!F1Z!~_>u?nta04506Ps|GtM6h99$+i}!VWydPCUXcibgfX@u!4`Uv){?OI@*#
zQm~)WaDdWrh{obDO~4V#LJdvBQJRlq<il|)#tB-CT3U*eRE1Nt9;azD&d_$ePt`a}
zHHc6x&QS#C$%ILl@gZHs1-glgbPFHR9bBP%xJvi&G5v{8=pjC(NBB%d<C==Yb(Mr0
z>M?w-Qt*Z9i<>G9U#fI`r6%BOH3{FSsko(P;<lQHZ&d-lQ^ojREyfRODekB$+*O<L
zquPdhsv1A51NcSN;8#_P-;{~p)g|0lSMWex!ykB=C)2I|=z$k`?C~LleCx<FxT=6>
zrmXpm!=S%;WDWy`WbpLhcDp_N7x#ZHVtL+0^#>lmUFGWum>X3GS9BfXOpL69`yw)C
z#h%BgI>d7@!3wsKpkW0)T-}ZniB_V$UEP6$Nmj6<U7aivtUq%{q7|>BS%L;{BbGfU
zzZv4ug;zb%8vR+2X=sOGNW>_#=Z}tLeuH%4kBZKG`^9{%V)>0_+k-jyI}Ky_4WihN
PV|1{6iW#HWJ`MT@VySEe

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/nondet-static/My.java b/jbmc/regression/jbmc/nondet-static/My.java
new file mode 100644
index 00000000000..6e8d6d86eef
--- /dev/null
+++ b/jbmc/regression/jbmc/nondet-static/My.java
@@ -0,0 +1,238 @@
+public class My {
+  public static int val() { return 3; }
+
+  public static int p1;
+  public static int p2 = 1;
+  public static int p3;
+  static { p3 = 2; }
+  public static int p4 = val();
+  public static Integer p5 = new Integer(5);
+
+  public static final int pf1 = 1;
+  public static final int pf2;
+  static { pf2 = 2; }
+  public static final int pf3 = val();
+  public static final Integer pf4 = new Integer(4);
+
+  private static int pr1;
+  private static int pr2 = 1;
+  private static int pr3;
+  static { pr3 = 2; }
+  private static int pr4 = val();
+  private static Integer pr5 = new Integer(5);
+
+  private static final int prf1 = 1;
+  private static final int prf2;
+  static { prf2 = 2; }
+  private static final int prf3 = val();
+  private static final Integer prf4 = new Integer(4);
+
+  // for inner classes, the missing cases of the above fields do not compile
+  public class PInner {
+    public static final int pf1 = 1;
+
+    private static final int prf1 = 1;
+  }
+
+  public static class PSInner {
+    public static int p1;
+    public static int p2 = 1;
+    public static int p3;
+    static { p3 = 2; }
+    public static int p4 = val();
+    public static Integer p5 = new Integer(5);
+
+    public static final int pf1 = 1;
+    public static final int pf2;
+    static { pf2 = 2; }
+    public static final int pf3 = val();
+    public static final Integer pf4 = new Integer(4);
+
+    private static int pr1;
+    private static int pr2 = 1;
+    private static int pr3;
+    static { pr3 = 2; }
+    private static int pr4 = val();
+    private static Integer pr5 = new Integer(5);
+
+    private static final int prf1 = 1;
+    private static final int prf2;
+    static { prf2 = 2; }
+    private static final int prf3 = val();
+    private static final Integer prf4 = new Integer(4);
+  }
+
+  private class PrInner {
+    public static final int pf1 = 1;
+
+    private static final int prf1 = 1;
+  }
+
+  private static class PrSInner {
+    public static int p1;
+    public static int p2 = 1;
+    public static int p3;
+    static { p3 = 2; }
+    public static int p4 = val();
+    public static Integer p5 = new Integer(5);
+
+    public static final int pf1 = 1;
+    public static final int pf2;
+    static { pf2 = 2; }
+    public static final int pf3 = val();
+    public static final Integer pf4 = new Integer(4);
+
+    private static int pr1;
+    private static int pr2 = 1;
+    private static int pr3;
+    static { pr3 = 2; }
+    private static int pr4 = val();
+    private static Integer pr5 = new Integer(5);
+
+    private static final int prf1 = 1;
+    private static final int prf2;
+    static { prf2 = 2; }
+    private static final int prf3 = val();
+    private static final Integer prf4 = new Integer(4);
+  }
+
+  public int field;
+  public My(int i) {
+    String s = "bla";
+    field = i;
+    if (p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PSInner.p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PSInner.p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PSInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PSInner.pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PSInner.pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PSInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrSInner.p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PrSInner.p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PrSInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PrSInner.pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrSInner.pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PrSInner.pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PrSInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (s != "bla")
+      field = 108; // this line cannot be covered even with nondet-static
+  }
+}
diff --git a/jbmc/regression/jbmc/nondet-static/test.desc b/jbmc/regression/jbmc/nondet-static/test.desc
new file mode 100644
index 00000000000..36b8fd59718
--- /dev/null
+++ b/jbmc/regression/jbmc/nondet-static/test.desc
@@ -0,0 +1,70 @@
+CORE symex-driven-lazy-loading-expected-failure
+My.class
+--function "My.<init>" --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+file My\.java line 104 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 106 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 108 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 110 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 112 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 117 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 119 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 121 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 124 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 126 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 128 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 130 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 132 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 137 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 139 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 141 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 150 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 152 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 154 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 156 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 158 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 163 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 165 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 167 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 170 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 172 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 174 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 176 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 178 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 183 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 185 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 187 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 196 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 198 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 200 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 202 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 204 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 209 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 211 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 213 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 216 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 218 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 220 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 222 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 224 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 229 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 231 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 233 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 236 function java::My\.\<init\>:\(I\)V.*FAILED$
+--
+file My\.java line 115 function java::My\.\<init\>:\(I\)V
+file My\.java line 135 function java::My\.\<init\>:\(I\)V
+file My\.java line 144 function java::My\.\<init\>:\(I\)V
+file My\.java line 147 function java::My\.\<init\>:\(I\)V
+file My\.java line 161 function java::My\.\<init\>:\(I\)V
+file My\.java line 181 function java::My\.\<init\>:\(I\)V
+file My\.java line 190 function java::My\.\<init\>:\(I\)V
+file My\.java line 193 function java::My\.\<init\>:\(I\)V
+file My\.java line 207 function java::My\.\<init\>:\(I\)V
+file My\.java line 227 function java::My\.\<init\>:\(I\)V
+--
+This tests nondet-static option
+
+This fails under symex-driven lazy loading because nondet-static cannot be used
+with it

From 437be99cba5b970b5c8d4ca81d68118779d09c47 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Wed, 8 Aug 2018 15:06:03 +0100
Subject: [PATCH 7/8] Perform nondet-init in clinit_wrapper even if clinit
 doesn't exist

This just moves the whole if(nondet-static) block outside of the
if(find_sym_it != symbol_table.symbols.end()) block and updates the
comment
---
 .../java_static_initializers.cpp              | 86 +++++++++----------
 1 file changed, 43 insertions(+), 43 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index dda21f4c971..2c1d1c27346 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -220,51 +220,51 @@ static void clinit_wrapper_do_recursive_calls(
     code_function_callt call_real_init;
     call_real_init.function() = find_sym_it->second.symbol_expr();
     init_body.move_to_operands(call_real_init);
+  }
 
-    // Add a standard nondet initialization for each non-final static field
-    // of this class. Note this is the same invocation used in
-    // get_stub_initializer_body and java_static_lifetime_init.
-    if(nondet_static)
+  // If nondet-static option is given, add a standard nondet initialization for
+  // each non-final static field of this class. Note this is the same invocation
+  // used in get_stub_initializer_body and java_static_lifetime_init.
+  if(nondet_static)
+  {
+    object_factory_parameterst parameters = object_factory_parameters;
+    parameters.function_id = clinit_wrapper_name(class_name);
+
+    std::vector<irep_idt> nondet_ids;
+    std::for_each(
+      symbol_table.symbols.begin(),
+      symbol_table.symbols.end(),
+      [&](const std::pair<irep_idt, symbolt> &symbol) {
+        if(
+          symbol.second.type.get(ID_C_class) == class_name &&
+          symbol.second.is_static_lifetime &&
+          !symbol.second.type.get_bool(ID_C_constant))
+        {
+          nondet_ids.push_back(symbol.first);
+        }
+      });
+
+    for(const auto &id : nondet_ids)
     {
-      object_factory_parameterst parameters = object_factory_parameters;
-      parameters.function_id = clinit_wrapper_name(class_name);
-
-      std::vector<irep_idt> nondet_ids;
-      std::for_each(
-        symbol_table.symbols.begin(),
-        symbol_table.symbols.end(),
-        [&](const std::pair<irep_idt, symbolt> &symbol) {
-          if(
-            symbol.second.type.get(ID_C_class) == class_name &&
-            symbol.second.is_static_lifetime &&
-            !symbol.second.type.get_bool(ID_C_constant))
-          {
-            nondet_ids.push_back(symbol.first);
-          }
-        });
-
-      for(const auto &id : nondet_ids)
-      {
-        const symbol_exprt new_global_symbol =
-          symbol_table.lookup_ref(id).symbol_expr();
-
-        parameters.max_nonnull_tree_depth =
-          is_non_null_library_global(id)
-            ? std::max(
-                size_t(1), object_factory_parameters.max_nonnull_tree_depth)
-            : object_factory_parameters.max_nonnull_tree_depth;
-
-        gen_nondet_init(
-          new_global_symbol,
-          init_body,
-          symbol_table,
-          source_locationt(),
-          false,
-          allocation_typet::DYNAMIC,
-          parameters,
-          pointer_type_selector,
-          update_in_placet::NO_UPDATE_IN_PLACE);
-      }
+      const symbol_exprt new_global_symbol =
+        symbol_table.lookup_ref(id).symbol_expr();
+
+      parameters.max_nonnull_tree_depth =
+        is_non_null_library_global(id)
+          ? std::max(
+              size_t(1), object_factory_parameters.max_nonnull_tree_depth)
+          : object_factory_parameters.max_nonnull_tree_depth;
+
+      gen_nondet_init(
+        new_global_symbol,
+        init_body,
+        symbol_table,
+        source_locationt(),
+        false,
+        allocation_typet::DYNAMIC,
+        parameters,
+        pointer_type_selector,
+        update_in_placet::NO_UPDATE_IN_PLACE);
     }
   }
 }

From e37d051c223aca235e6a29c4c44140841b8074be Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Tue, 14 Aug 2018 17:31:06 +0100
Subject: [PATCH 8/8] Add a comment to static field with the name of the field

---
 jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 1 +
 src/util/irep_ids.def                                  | 1 +
 2 files changed, 2 insertions(+)

diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 46beec8965b..f8bc2e396bc 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -645,6 +645,7 @@ void java_bytecode_convert_classt::convert(
     // link matches the method used by java_bytecode_convert_method::convert
     // for methods.
     new_symbol.type.set(ID_C_class, class_symbol.name);
+    new_symbol.type.set(ID_C_field, f.name);
     new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
       "."+id2string(f.name);
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 42a1d7c447f..321802c8abe 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -351,6 +351,7 @@ IREP_ID_TWO(power, **)
 IREP_ID_ONE(factorial_power)
 IREP_ID_ONE(pretty_name)
 IREP_ID_TWO(C_class, #class)
+IREP_ID_TWO(C_field, #field)
 IREP_ID_TWO(C_interface, #interface)
 IREP_ID_ONE(event)
 IREP_ID_ONE(designated_initializer)