Merge pull request #3246 from danpoe/fixes/rename-max-nonnull-tree-depth

Fix misleading struct member name in Java object factory

Author: danpoe

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -100,7 +100,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
     const auto &nondet_expr = to_side_effect_expr_nondet(op);
 
     if(!nondet_expr.get_nullable())
-      object_factory_parameters.max_nonnull_tree_depth = 1;
+      object_factory_parameters.min_null_tree_depth = 1;
 
     const source_locationt &source_loc = target->source_location;
 

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -219,7 +219,7 @@ static void java_static_lifetime_init(
 
         object_factory_parameterst parameters = object_factory_parameters;
         if(not_allow_null && !is_class_model)
-          parameters.max_nonnull_tree_depth = 1;
+          parameters.min_null_tree_depth = 1;
 
         gen_nondet_init(
           sym.symbol_expr(),
@@ -309,10 +309,10 @@ exprt::operandst java_build_arguments(
     object_factory_parameterst parameters = object_factory_parameters;
     // only pointer must be non-null
     if(assume_init_pointers_not_null || is_this)
-      parameters.max_nonnull_tree_depth = 1;
+      parameters.min_null_tree_depth = 1;
     // in main() also the array elements of the argument must be non-null
     if(is_main)
-      parameters.max_nonnull_tree_depth = 2;
+      parameters.min_null_tree_depth = 2;
 
     parameters.function_id = goto_functionst::entry_point();
 

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -860,8 +860,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
-  const bool allow_null =
-    depth > object_factory_parameters.max_nonnull_tree_depth;
+  const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
 
   if(must_be_null)
   {

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -248,11 +248,10 @@ static void clinit_wrapper_do_recursive_calls(
       const symbol_exprt new_global_symbol =
         symbol_table.lookup_ref(id).symbol_expr();
 
-      parameters.max_nonnull_tree_depth =
+      parameters.min_null_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;
+          ? std::max(size_t(1), object_factory_parameters.min_null_tree_depth)
+          : object_factory_parameters.min_null_tree_depth;
 
       gen_nondet_init(
         new_global_symbol,
@@ -872,10 +871,10 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
     const symbol_exprt new_global_symbol =
       symbol_table.lookup_ref(it->second).symbol_expr();
 
-    parameters.max_nonnull_tree_depth =
+    parameters.min_null_tree_depth =
       is_non_null_library_global(it->second)
-        ? object_factory_parameters.max_nonnull_tree_depth + 1
-        : object_factory_parameters.max_nonnull_tree_depth;
+        ? object_factory_parameters.min_null_tree_depth + 1
+        : object_factory_parameters.min_null_tree_depth;
 
     source_locationt location;
     location.set_function(function_id);

jbmc/src/java_bytecode/object_factory_parameters.h

@@ -21,7 +21,7 @@ class optionst;
 #define MAX_NONDET_STRING_LENGTH \
   static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max())
 #define MAX_NONDET_TREE_DEPTH 5
-#define MAX_NONNULL_TREE_DEPTH 0
+#define MIN_NULL_TREE_DEPTH 0
 
 struct object_factory_parameterst final
 {
@@ -45,14 +45,14 @@ struct object_factory_parameterst final
   /// To force a certain depth of non-null objects.
   /// The default is that objects are 'maybe null' up to the nondet tree depth.
   /// Examples:
-  /// * max_nondet_tree_depth=0, max_nonnull_tree_depth irrelevant
+  /// * max_nondet_tree_depth=0, min_null_tree_depth irrelevant
   ///   pointer initialized to null
-  /// * max_nondet_tree_depth=n, max_nonnull_tree_depth=0
+  /// * max_nondet_tree_depth=n, min_null_tree_depth=0
   ///   pointer and children up to depth n maybe-null, beyond n null
-  /// * max_nondet_tree_depth=n >=m, max_nonnull_tree_depth=m
+  /// * max_nondet_tree_depth=n >=m, min_null_tree_depth=m
   ///   pointer and children up to depth m initialized to non-null,
   ///   children up to n maybe-null, beyond n null
-  size_t max_nonnull_tree_depth = MAX_NONNULL_TREE_DEPTH;
+  size_t min_null_tree_depth = MIN_NULL_TREE_DEPTH;
 
   /// Force string content to be ASCII printable characters when set to true.
   bool string_printable = false;

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -110,7 +110,7 @@ void java_simple_method_stubst::create_method_stub_at(
 
   object_factory_parameterst parameters = object_factory_parameters;
   if(assume_non_null)
-    parameters.max_nonnull_tree_depth = 1;
+    parameters.min_null_tree_depth = 1;
 
   // Generate new instructions.
   code_blockt new_instructions;
@@ -198,7 +198,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       {
         object_factory_parameterst parameters = object_factory_parameters;
         if(assume_non_null)
-          parameters.max_nonnull_tree_depth = 1;
+          parameters.min_null_tree_depth = 1;
 
         gen_nondet_init(
           to_return,