cprover
|
#include <object_factory_parameters.h>
Public Attributes | |
size_t | max_nondet_array_length = 5 |
Maximum value for the non-deterministically-chosen length of an array. More... | |
size_t | max_nondet_string_length = static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max()) |
Maximum value for the non-deterministically-chosen length of a string. More... | |
size_t | max_nondet_tree_depth = 5 |
Maximum depth for object hierarchy on input. More... | |
size_t | max_nonnull_tree_depth = 0 |
To force a certain depth of non-null objects. More... | |
bool | string_printable = false |
Force string content to be ASCII printable characters when set to true. More... | |
irep_idt | function_id |
Function id, used as a prefix for identifiers of temporaries. More... | |
Definition at line 23 of file object_factory_parameters.h.
irep_idt object_factory_parameterst::function_id |
Function id, used as a prefix for identifiers of temporaries.
Definition at line 55 of file object_factory_parameters.h.
Referenced by java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), convert_nondet(), java_simple_method_stubst::create_method_stub_at(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_nondet_subtype_pointer_init(), stub_global_initializer_factoryt::get_stub_initializer_body(), java_build_arguments(), java_static_lifetime_init(), and object_factory().
size_t object_factory_parameterst::max_nondet_array_length = 5 |
Maximum value for the non-deterministically-chosen length of an array.
Definition at line 26 of file object_factory_parameters.h.
Referenced by jbmc_parse_optionst::doit(), java_object_factoryt::gen_nondet_array_init(), and java_bytecode_languaget::get_language_options().
size_t object_factory_parameterst::max_nondet_string_length = static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max()) |
Maximum value for the non-deterministically-chosen length of a string.
Definition at line 29 of file object_factory_parameters.h.
Referenced by jbmc_parse_optionst::doit(), java_object_factoryt::gen_nondet_struct_init(), and java_bytecode_languaget::get_language_options().
size_t object_factory_parameterst::max_nondet_tree_depth = 5 |
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.
Definition at line 37 of file object_factory_parameters.h.
Referenced by jbmc_parse_optionst::doit(), java_object_factoryt::gen_nondet_pointer_init(), and java_bytecode_languaget::get_language_options().
size_t object_factory_parameterst::max_nonnull_tree_depth = 0 |
To force a certain depth of non-null objects.
The default is that objects are 'maybe null' up to the nondet tree depth. Examples:
Definition at line 49 of file object_factory_parameters.h.
Referenced by java_simple_method_stubst::create_method_stub(), java_simple_method_stubst::create_method_stub_at(), java_object_factoryt::gen_nondet_pointer_init(), stub_global_initializer_factoryt::get_stub_initializer_body(), insert_nondet_init_code(), java_build_arguments(), and java_static_lifetime_init().
bool object_factory_parameterst::string_printable = false |
Force string content to be ASCII printable characters when set to true.
Definition at line 52 of file object_factory_parameters.h.
Referenced by java_object_factoryt::gen_nondet_struct_init(), and java_bytecode_languaget::get_language_options().