#include <object_factory_parameters.h>
Inheritance diagram for object_factory_parameterst: Collaboration diagram for object_factory_parameterst:Public Member Functions | |
| object_factory_parameterst () | |
| object_factory_parameterst (const optionst &options) | |
| virtual | ~object_factory_parameterst ()=default |
| void | set (const optionst &) |
| Assigns the parameters from given options. More... | |
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 = MAX_CONCRETE_STRING_SIZE - 1 |
| Maximum value for the non-deterministically-chosen length of a string. More... | |
| size_t | min_nondet_string_length = 0 |
| Minimum value for the non-deterministically-chosen length of a string. More... | |
| size_t | max_nondet_tree_depth = 5 |
| Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects. More... | |
| size_t | min_null_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... | |
| std::list< std::string > | string_input_values |
| Force one of finitely many explicitly given input strings. More... | |
| irep_idt | function_id |
| Function id, used as a prefix for identifiers of temporaries. More... | |
Detailed Description
Definition at line 20 of file object_factory_parameters.h.
Constructor & Destructor Documentation
◆ object_factory_parameterst() [1/2]
|
inline |
Definition at line 22 of file object_factory_parameters.h.
◆ object_factory_parameterst() [2/2]
|
inlineexplicit |
Definition at line 26 of file object_factory_parameters.h.
◆ ~object_factory_parameterst()
|
virtualdefault |
Member Function Documentation
◆ set()
| void object_factory_parameterst::set | ( | const optionst & | options | ) |
Assigns the parameters from given options.
Definition at line 14 of file object_factory_parameters.cpp.
Member Data Documentation
◆ function_id
| irep_idt object_factory_parameterst::function_id |
Function id, used as a prefix for identifiers of temporaries.
Definition at line 79 of file object_factory_parameters.h.
◆ 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 34 of file object_factory_parameters.h.
◆ max_nondet_string_length
| size_t object_factory_parameterst::max_nondet_string_length = MAX_CONCRETE_STRING_SIZE - 1 |
Maximum value for the non-deterministically-chosen length of a string.
Defaults to MAX_CONCRETE_STRING_SIZE - 1 such that even with a null terminator all strings can be rendered concretely by string-refinement's get_array function, which is used by --trace among other C/JBMC options.
Definition at line 41 of file object_factory_parameters.h.
◆ max_nondet_tree_depth
| size_t object_factory_parameterst::max_nondet_tree_depth = 5 |
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
Used to prevent the object factory from looping infinitely during the generation of code that allocates/initializes recursive data structures (such as a linked list). The object factory tracks the number of times a pointer has been dereferenced in a 'depth' counter variable. If a pointer to be initialized points to an object of a type that already occured on the current pointer chain, and if 'depth' is larger than 'max_nondet_tree_depth`, then the pointer is set to null. The parameter does not affect non-recursive data structures, which are always initialized to their full depth.
Definition at line 58 of file object_factory_parameters.h.
◆ min_nondet_string_length
| size_t object_factory_parameterst::min_nondet_string_length = 0 |
Minimum value for the non-deterministically-chosen length of a string.
Definition at line 44 of file object_factory_parameters.h.
◆ min_null_tree_depth
| size_t object_factory_parameterst::min_null_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, min_null_tree_depth irrelevant pointer initialized to null
- 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, 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
Definition at line 70 of file object_factory_parameters.h.
◆ string_input_values
| std::list<std::string> object_factory_parameterst::string_input_values |
Force one of finitely many explicitly given input strings.
Definition at line 76 of file object_factory_parameters.h.
◆ string_printable
| bool object_factory_parameterst::string_printable = false |
Force string content to be ASCII printable characters when set to true.
Definition at line 73 of file object_factory_parameters.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/util/object_factory_parameters.h
- /home/runner/work/cbmc/cbmc/src/util/object_factory_parameters.cpp
