Configuration used for a symbolic execution. More...

#include <symex_config.h>

Public Member Functions
	symex_configt (const optionst &options)
	Construct a symex_configt using options specified in an optionst. More...

Public Attributes
unsigned	max_depth
	The maximum depth to take the execution to. More...

bool	doing_path_exploration

bool	allow_pointer_unsoundness

bool	constant_propagation

bool	self_loops_to_assumptions

bool	simplify_opt

bool	unwinding_assertions

bool	partial_loops

bool	run_validation_checks
	Should the additional validation checks be run? If this flag is set the checks for renaming (both level1 and level2) are executed in the goto_symex_statet (in the assignment method). More...

bool	show_symex_steps
	Prints out the path that symex is actively taking during execution, includes diagnostic information about call stack and guard size. More...

bool	show_points_to_sets

std::size_t	max_field_sensitivity_array_size
	Maximum sizes for which field sensitivity will be applied to array cells. More...

bool	complexity_limits_active
	Whether this run of symex is under complexity limits. More...

bool	cache_dereferences
	Whether or not to replace multiple occurrences of the same dereference with a single symbol that contains the result of that dereference. More...

Detailed Description

Configuration used for a symbolic execution.

Definition at line 18 of file symex_config.h.

Constructor & Destructor Documentation

◆ symex_configt()

symex_configt::symex_configt ( const optionst & options )

explicit

Construct a symex_configt using options specified in an optionst.

Definition at line 30 of file symex_main.cpp.

Member Data Documentation

◆ allow_pointer_unsoundness

bool symex_configt::allow_pointer_unsoundness

Definition at line 27 of file symex_config.h.

◆ cache_dereferences

bool symex_configt::cache_dereferences

Whether or not to replace multiple occurrences of the same dereference with a single symbol that contains the result of that dereference.

Can sometimes lead to a significant performance improvement, but sometimes also makes things worse. See https://github.com/diffblue/cbmc/pull/5964 for performance data. Used in goto_symext::dereference_rec

Definition at line 62 of file symex_config.h.

◆ complexity_limits_active

bool symex_configt::complexity_limits_active

Whether this run of symex is under complexity limits.

This enables certain analyses that otherwise aren't run.

Definition at line 54 of file symex_config.h.

◆ constant_propagation

bool symex_configt::constant_propagation

Definition at line 29 of file symex_config.h.

◆ doing_path_exploration

bool symex_configt::doing_path_exploration

Definition at line 25 of file symex_config.h.

◆ max_depth

unsigned symex_configt::max_depth

The maximum depth to take the execution to.

Depth is a count of the instructions that have been executed on any single path.

Definition at line 23 of file symex_config.h.

◆ max_field_sensitivity_array_size

std::size_t symex_configt::max_field_sensitivity_array_size

Maximum sizes for which field sensitivity will be applied to array cells.

Definition at line 50 of file symex_config.h.

◆ partial_loops

bool symex_configt::partial_loops

Definition at line 37 of file symex_config.h.

◆ run_validation_checks

bool symex_configt::run_validation_checks

Should the additional validation checks be run? If this flag is set the checks for renaming (both level1 and level2) are executed in the goto_symex_statet (in the assignment method).

Definition at line 42 of file symex_config.h.

◆ self_loops_to_assumptions

bool symex_configt::self_loops_to_assumptions

Definition at line 31 of file symex_config.h.

◆ show_points_to_sets

bool symex_configt::show_points_to_sets

Definition at line 47 of file symex_config.h.

◆ show_symex_steps

bool symex_configt::show_symex_steps

Prints out the path that symex is actively taking during execution, includes diagnostic information about call stack and guard size.

Definition at line 46 of file symex_config.h.

◆ simplify_opt

bool symex_configt::simplify_opt

Definition at line 33 of file symex_config.h.

◆ unwinding_assertions

bool symex_configt::unwinding_assertions

Definition at line 35 of file symex_config.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/symex_config.h
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_main.cpp

Public Member Functions

Public Attributes