diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.class b/regression/strings-smoke-tests/max_input_length/MemberTest.class new file mode 100644 index 00000000000..cbb5dcfdbbd Binary files /dev/null and b/regression/strings-smoke-tests/max_input_length/MemberTest.class differ diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/regression/strings-smoke-tests/max_input_length/MemberTest.desc new file mode 100644 index 00000000000..7bc3ccc6c86 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/MemberTest.desc @@ -0,0 +1,7 @@ +CORE +MemberTest.class +--refine-strings --string-max-length 29 --java-assume-inputs-non-null +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.java b/regression/strings-smoke-tests/max_input_length/MemberTest.java new file mode 100644 index 00000000000..cf88d8d8f83 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/MemberTest.java @@ -0,0 +1,9 @@ +public class MemberTest { + String foo; + public void main() { + // Causes this function to be ignored if string-max-length is + // less than 40 + String t = new String("0123456789012345678901234567890123456789"); + assert foo != null && foo.length() < 30; + } +} diff --git a/regression/strings-smoke-tests/max_input_length/Test.class b/regression/strings-smoke-tests/max_input_length/Test.class new file mode 100644 index 00000000000..d01720ffa38 Binary files /dev/null and b/regression/strings-smoke-tests/max_input_length/Test.class differ diff --git a/regression/strings-smoke-tests/max_input_length/Test.java b/regression/strings-smoke-tests/max_input_length/Test.java new file mode 100644 index 00000000000..0616daa4053 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/Test.java @@ -0,0 +1,11 @@ +public class Test { + public static void main(String s) { + // This prevent anything from happening if string-max-length is smaller + // than 40 + String t = new String("0123456789012345678901234567890123456789"); + if (s.length() >= 30) + // This should not happen when string-max-input length is smaller + // than 30 + assert false; + } +} diff --git a/regression/strings-smoke-tests/max_input_length/test.desc b/regression/strings-smoke-tests/max_input_length/test.desc new file mode 100644 index 00000000000..0fddf482a9c --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/test.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --string-max-length 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/max_input_length/test1.desc b/regression/strings-smoke-tests/max_input_length/test1.desc new file mode 100644 index 00000000000..00bda639119 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/test1.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --string-max-length 45 --string-max-input-length 31 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/strings-smoke-tests/max_input_length/test2.desc b/regression/strings-smoke-tests/max_input_length/test2.desc new file mode 100644 index 00000000000..8aaaf205c92 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/test2.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --string-max-length 45 --string-max-input-length 20 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index aa2736cb862..bdd8c10c8e7 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -793,11 +793,16 @@ bool cbmc_parse_optionst::process_goto_program( // Similar removal of java nondet statements: // TODO Should really get this from java_bytecode_language somehow, but we // don't have an instance of that here. - const size_t max_nondet_array_length= + object_factory_parameterst factory_params; + factory_params.max_nondet_array_length= cmdline.isset("java-max-input-array-length") ? std::stoul(cmdline.get_value("java-max-input-array-length")) : MAX_NONDET_ARRAY_LENGTH_DEFAULT; - const size_t max_nondet_tree_depth= + factory_params.max_nondet_string_length= + cmdline.isset("string-max-input-length") + ? std::stoul(cmdline.get_value("string-max-input-length")) + : MAX_NONDET_STRING_LENGTH; + factory_params.max_nondet_tree_depth= cmdline.isset("java-max-input-tree-depth") ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) : MAX_NONDET_TREE_DEPTH; @@ -807,8 +812,7 @@ bool cbmc_parse_optionst::process_goto_program( convert_nondet( goto_model, get_message_handler(), - max_nondet_array_length, - max_nondet_tree_depth); + factory_params); // add generic checks status() << "Generic Property Instrumentation" << eom; @@ -1067,7 +1071,8 @@ void cbmc_parse_optionst::help() " --refine-strings use string refinement (experimental)\n" " --string-non-empty add constraint that strings are non empty (experimental)\n" // NOLINT(*) " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) - " --string-max-length add constraint on the length of strings (experimental)\n" // NOLINT(*) + " --string-max-length add constraint on the length of strings\n" // NOLINT(*) + " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 85461fef191..08a0ef619ab 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -48,6 +48,7 @@ class optionst; "(string-non-empty)" \ "(string-printable)" \ "(string-max-length):" \ + "(string-max-input-length):" \ "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index b329a41ddbc..23643f26bc6 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -34,8 +34,7 @@ static goto_programt::targett insert_nondet_init_code( const goto_programt::targett &target, symbol_tablet &symbol_table, message_handlert &message_handler, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth) + const object_factory_parameterst &object_factory_parameters) { // Return if the instruction isn't an assignment const auto next_instr=std::next(target); @@ -91,8 +90,7 @@ static goto_programt::targett insert_nondet_init_code( true, allocation_typet::DYNAMIC, nullable, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, update_in_placet::NO_UPDATE_IN_PLACE); // Convert this code into goto instructions @@ -117,8 +115,7 @@ void convert_nondet( goto_programt &goto_program, symbol_tablet &symbol_table, message_handlert &message_handler, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth) + const object_factory_parameterst &object_factory_parameters) { for(auto instruction_iterator=goto_program.instructions.begin(), end=goto_program.instructions.end(); @@ -129,8 +126,7 @@ void convert_nondet( instruction_iterator, symbol_table, message_handler, - max_nondet_array_length, - max_nondet_tree_depth); + object_factory_parameters); } } @@ -138,8 +134,7 @@ void convert_nondet( goto_functionst &goto_functions, symbol_tablet &symbol_table, message_handlert &message_handler, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth) + const object_factory_parameterst &object_factory_parameters) { for(auto &goto_program : goto_functions.function_map) { @@ -147,8 +142,7 @@ void convert_nondet( goto_program.second.body, symbol_table, message_handler, - max_nondet_array_length, - max_nondet_tree_depth); + object_factory_parameters); } goto_functions.compute_location_numbers(); @@ -159,13 +153,11 @@ void convert_nondet( void convert_nondet( goto_modelt &goto_model, message_handlert &message_handler, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth) + const object_factory_parameterst& object_factory_parameters) { convert_nondet( goto_model.goto_functions, goto_model.symbol_table, message_handler, - max_nondet_array_length, - max_nondet_tree_depth); + object_factory_parameters); } diff --git a/src/goto-programs/convert_nondet.h b/src/goto-programs/convert_nondet.h index 32d8cd33f91..95b48ae5dd7 100644 --- a/src/goto-programs/convert_nondet.h +++ b/src/goto-programs/convert_nondet.h @@ -18,26 +18,24 @@ class goto_functionst; class symbol_tablet; class goto_modelt; class message_handlert; +struct object_factory_parameterst; /// Replace calls to nondet library functions with an internal nondet /// representation. /// \param goto_functions: The set of goto programs to modify. /// \param symbol_table: The symbol table to query/update. /// \param message_handler: For error logging. -/// \param max_nondet_array_length: The maximum length of any new arrays. -/// \param max_nondet_tree_depth: Maximum depth for object hierarchy on input -/// parameterers. +/// \param object_factory_parameters: Parameters for the generation of nondet +/// objects. void convert_nondet( goto_functionst &, symbol_tablet &, message_handlert &, - std::size_t max_nondet_array_length, - std::size_t max_nondet_tree_depth); + const object_factory_parameterst &object_factory_parameters); void convert_nondet( goto_modelt &, message_handlert &, - std::size_t max_nondet_array_length, - std::size_t max_nondet_tree_depth); + const object_factory_parameterst &object_factory_parameters); #endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 8ea79aafa6d..74d527ab8ad 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -42,11 +42,14 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) string_refinement_enabled=cmd.isset("refine-strings"); throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); if(cmd.isset("java-max-input-array-length")) - max_nondet_array_length= + object_factory_parameters.max_nondet_array_length= std::stoi(cmd.get_value("java-max-input-array-length")); if(cmd.isset("java-max-input-tree-depth")) - max_nondet_tree_depth= + object_factory_parameters.max_nondet_tree_depth= std::stoi(cmd.get_value("java-max-input-tree-depth")); + if(cmd.isset("string-max-input-length")) + object_factory_parameters.max_nondet_string_length= + std::stoi(cmd.get_value("string-max-input-length")); if(cmd.isset("java-max-vla-length")) max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); if(cmd.isset("lazy-methods-context-sensitive")) @@ -125,8 +128,7 @@ bool java_bytecode_languaget::generate_start_function( symbol_table, get_message_handler(), assume_inputs_non_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, *pointer_type_selector); } @@ -402,8 +404,7 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table) main_class, get_message_handler(), assume_inputs_non_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, get_pointer_type_selector()); } diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 21cacce6465..dd2a20eaafe 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -48,6 +48,7 @@ Author: Daniel Kroening, kroening@kroening.com " A '.*' wildcard is allowed to specify all class members\n" #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 +#define MAX_NONDET_STRING_LENGTH std::numeric_limits::max() #define MAX_NONDET_TREE_DEPTH 5 class symbolt; @@ -59,6 +60,23 @@ enum lazy_methods_modet LAZY_METHODS_MODE_CONTEXT_SENSITIVE }; +struct object_factory_parameterst final +{ + /// Maximum value for the non-deterministically-chosen length of an array. + size_t max_nondet_array_length=MAX_NONDET_ARRAY_LENGTH_DEFAULT; + + /// Maximum value for the non-deterministically-chosen length of a string. + size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH; + + /// Maximum depth for object hierarchy on input. + /// Used to prevent object factory to loop infinitely during the + /// generation of code that allocates/initializes data structures of recursive + /// data types or unbounded depth. We bound the maximum number of times we + /// dereference a pointer using a 'depth counter'. We set a pointer to null if + /// such depth becomes >= than this maximum value. + size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH; +}; + typedef std::pair< const symbolt *, const java_bytecode_parse_treet::methodt *> @@ -95,8 +113,7 @@ class java_bytecode_languaget:public languaget java_bytecode_languaget( std::unique_ptr pointer_type_selector): assume_inputs_non_null(false), - max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT), - max_nondet_tree_depth(MAX_NONDET_TREE_DEPTH), + object_factory_parameters(), max_user_array_length(0), lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER), string_refinement_enabled(false), @@ -149,8 +166,7 @@ class java_bytecode_languaget:public languaget std::vector main_jar_classes; java_class_loadert java_class_loader; bool assume_inputs_non_null; // assume inputs variables to be non-null - size_t max_nondet_array_length; // maximal length for non-det array creation - size_t max_nondet_tree_depth; // maximal depth for object tree in non-det creation + object_factory_parameterst object_factory_parameters; size_t max_user_array_length; // max size for user code created arrays lazy_methodst lazy_methods; lazy_methods_modet lazy_methods_mode; diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 12e806b8e2f..e456556c258 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -90,8 +90,7 @@ void java_static_lifetime_init( symbol_tablet &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, - unsigned max_nondet_array_length, - unsigned max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE); @@ -132,8 +131,7 @@ void java_static_lifetime_init( code_block, allow_null, symbol_table, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, allocation_typet::GLOBAL, source_location, pointer_type_selector); @@ -164,8 +162,7 @@ exprt::operandst java_build_arguments( code_blockt &init_code, symbol_tablet &symbol_table, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector) { const code_typet::parameterst ¶meters= @@ -221,8 +218,7 @@ exprt::operandst java_build_arguments( init_code, allow_null, symbol_table, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, allocation_typet::LOCAL, function.location, pointer_type_selector); @@ -481,8 +477,7 @@ bool java_entry_point( const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { // check if the entry point is already there @@ -506,8 +501,7 @@ bool java_entry_point( symbol_table, symbol.location, assume_init_pointers_not_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector); return generate_java_start_function( @@ -515,8 +509,7 @@ bool java_entry_point( symbol_table, message_handler, assume_init_pointers_not_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector); } @@ -538,8 +531,7 @@ bool generate_java_start_function( symbol_tablet &symbol_table, message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst& object_factory_parameters, const select_pointer_typet &pointer_type_selector) { messaget message(message_handler); @@ -618,8 +610,7 @@ bool generate_java_start_function( init_code, symbol_table, assume_init_pointers_not_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector); call_main.arguments()=main_arguments; diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index cc03e8480b5..9461a4a826d 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'" #define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'" @@ -22,8 +23,7 @@ bool java_entry_point( const irep_idt &main_class, class message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector); typedef struct @@ -45,8 +45,7 @@ bool generate_java_start_function( class symbol_tablet &symbol_table, class message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst& object_factory_parameters, const select_pointer_typet &pointer_type_selector); #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index b9e3da19651..ff2ae2784eb 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -58,15 +58,7 @@ class java_object_factoryt /// methods in this class. const source_locationt &loc; - /// Maximum value for the non-deterministically-chosen length of an array. - const size_t max_nondet_array_length; - - /// Used to prevent the methods in this class to loop infinitely during the - /// generation of code that allocates/initializes data structures of recursive - /// data types or unbounded depth. We bound the maximum number of times we - /// dereference a pointer using a 'depth counter'. We set a pointer to null if - /// such depth becomes >= than this maximum value. - const size_t max_nondet_tree_depth; + const object_factory_parameterst object_factory_parameters; /// This is employed in conjunction with the depth above. Every time the /// non-det generator visits a type, the type is added to this set. We forbid @@ -107,14 +99,12 @@ class java_object_factoryt java_object_factoryt( std::vector &_symbols_created, const source_locationt &loc, - size_t _max_nondet_array_length, - size_t _max_nondet_tree_depth, + const object_factory_parameterst _object_factory_parameters, symbol_tablet &_symbol_table, const select_pointer_typet &pointer_type_selector): symbols_created(_symbols_created), loc(loc), - max_nondet_array_length(_max_nondet_array_length), - max_nondet_tree_depth(_max_nondet_tree_depth), + object_factory_parameters(_object_factory_parameters), symbol_table(_symbol_table), ns(_symbol_table), pointer_type_selector(pointer_type_selector) @@ -591,7 +581,7 @@ void java_object_factoryt::gen_nondet_pointer_init( // If this is a recursive type of some kind AND the depth is exceeded, set // the pointer to null. if(!recursion_set_entry.insert_entry(struct_tag) && - depth>=max_nondet_tree_depth) + depth>=object_factory_parameters.max_nondet_tree_depth) { if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE) { @@ -760,6 +750,19 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( return new_symbol.symbol_expr(); } +/// Get max value for an integral type +/// \param type: +/// Type to find maximum value for +/// \return Maximum integral valu +static size_t max_value(const typet& type) +{ + if(type.id()==ID_signedbv) + return std::numeric_limits::max(); + else if(type.id()==ID_unsignedbv) + return std::numeric_limits::max(); + UNREACHABLE; +} + /// Initializes an object tree rooted at `expr`, allocating child objects as /// necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE /// is set, re-initializes already-allocated objects. @@ -863,6 +866,30 @@ void java_object_factoryt::gen_nondet_struct_init( true, // allow_null always true for sub-objects depth, substruct_in_place); + + if(name=="length") + { + if(class_identifier=="java.lang.String" || + class_identifier=="java.lang.StringBuffer" || + class_identifier=="java.lang.StringBuilder") + { + if(object_factory_parameters.max_nondet_string_length <= + max_value(me.type())) + { + exprt max_length=from_integer( + object_factory_parameters.max_nondet_string_length, me.type()); + assignments.add(code_assumet( + binary_relation_exprt(me, ID_le, max_length))); + } + } + else + { + INVARIANT( + class_identifier!="java.lang.CharSequence" && + class_identifier!="java.lang.AbstractStringBuilder", + "Trying to initialize abstract class"); + } + } } } } @@ -1043,7 +1070,8 @@ void java_object_factoryt::gen_nondet_array_init( const typet &element_type= static_cast(expr.type().subtype().find(ID_C_element_type)); - auto max_length_expr=from_integer(max_nondet_array_length, java_int_type()); + auto max_length_expr=from_integer( + object_factory_parameters.max_nondet_array_length, java_int_type()); // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively // initialize its elements @@ -1198,8 +1226,7 @@ exprt object_factory( code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst ¶meters, allocation_typet alloc_type, const source_locationt &loc, const select_pointer_typet &pointer_type_selector) @@ -1226,8 +1253,7 @@ exprt object_factory( java_object_factoryt state( symbols_created, loc, - max_nondet_array_length, - max_nondet_tree_depth, + parameters, symbol_table, pointer_type_selector); code_blockt assignments; @@ -1279,12 +1305,8 @@ exprt object_factory( /// when \p allow_null is false (as this parameter is not inherited by /// subsequent recursive calls). Has no effect when \p expr is not /// pointer-typed. -/// \param max_nondet_array_length: -/// Upper bound on size of initialized arrays. -/// \param max_nondet_tree_depth: -/// Maximum depth in the object hirearchy (counted as the number of times a -/// pointer is deferenced) created by the initialization code that will be -/// emitted here. +/// \param object_factory_parameters: +/// Parameters for the generation of non deterministic objects. /// \param pointer_type_selector: /// The pointer_selector to use to resolve pointer types where required. /// \param update_in_place: @@ -1304,8 +1326,7 @@ void gen_nondet_init( bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place) { @@ -1314,8 +1335,7 @@ void gen_nondet_init( java_object_factoryt state( symbols_created, loc, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, symbol_table, pointer_type_selector); code_blockt assignments; @@ -1338,13 +1358,13 @@ void gen_nondet_init( } /// Call object_factory() above with a default (identity) pointer_type_selector -exprt object_factory(const typet &type, +exprt object_factory( + const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, allocation_typet alloc_type, const source_locationt &location) { @@ -1355,23 +1375,22 @@ exprt object_factory(const typet &type, init_code, allow_null, symbol_table, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, alloc_type, location, pointer_type_selector); } /// Call gen_nondet_init() above with a default (identity) pointer_type_selector -void gen_nondet_init(const exprt &expr, +void gen_nondet_init( + const exprt &expr, code_blockt &init_code, symbol_tablet &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place) { select_pointer_typet pointer_type_selector; @@ -1383,8 +1402,7 @@ void gen_nondet_init(const exprt &expr, skip_classid, alloc_type, allow_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector, update_in_place); } diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index c08b6341877..3e1c06c52e1 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -73,6 +73,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include /// Selects the kind of allocation used by java_object_factory et al. enum class allocation_typet @@ -91,8 +92,7 @@ exprt object_factory( code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst ¶meters, allocation_typet alloc_type, const source_locationt &location, const select_pointer_typet &pointer_type_selector); @@ -103,8 +103,7 @@ exprt object_factory( code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, allocation_typet alloc_type, const source_locationt &location); @@ -123,8 +122,7 @@ void gen_nondet_init( bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place); @@ -136,8 +134,7 @@ void gen_nondet_init( bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place); exprt allocate_dynamic_object(