cprover
object_factory_parameterst Struct Referencefinal

#include <object_factory_parameters.h>

Collaboration diagram for object_factory_parameterst:
[legend]

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 = 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...
 

Detailed Description

Definition at line 22 of file object_factory_parameters.h.

Member Data Documentation

◆ function_id

◆ max_nondet_array_length

size_t object_factory_parameterst::max_nondet_array_length = 5

Maximum value for the non-deterministically-chosen length of an array.

Definition at line 25 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().

◆ max_nondet_string_length

size_t object_factory_parameterst::max_nondet_string_length = std::numeric_limits<std::int32_t>::max()

Maximum value for the non-deterministically-chosen length of a string.

Definition at line 28 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().

◆ max_nondet_tree_depth

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 36 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().

◆ max_nonnull_tree_depth

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:

  • max_nondet_tree_depth=0, max_nonnull_tree_depth irrelevant pointer initialized to null
  • max_nondet_tree_depth=n, max_nonnull_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 pointer and children up to depth m initialized to non-null, children up to n maybe-null, beyond n null

Definition at line 48 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().

◆ string_printable

bool object_factory_parameterst::string_printable = false

Force string content to be ASCII printable characters when set to true.

Definition at line 51 of file object_factory_parameters.h.

Referenced by java_object_factoryt::gen_nondet_pointer_init(), and java_bytecode_languaget::get_language_options().


The documentation for this struct was generated from the following file: