CBMC
object_factory_parameterst Struct Reference

#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]

object_factory_parameterst::object_factory_parameterst ( )
inline

Definition at line 22 of file object_factory_parameters.h.

◆ object_factory_parameterst() [2/2]

object_factory_parameterst::object_factory_parameterst ( const optionst options)
inlineexplicit

Definition at line 26 of file object_factory_parameters.h.

◆ ~object_factory_parameterst()

virtual object_factory_parameterst::~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: