CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_config.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution Config
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H
13#define CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H
14
15class optionst;
16
68
69#endif // CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H
Configuration used for a symbolic execution.
bool complexity_limits_active
Whether this run of symex is under complexity limits.
bool unwinding_assertions
bool show_points_to_sets
bool allow_pointer_unsoundness
bool constant_propagation
unsigned max_depth
The maximum depth to take the execution to.
bool self_loops_to_assumptions
bool cache_dereferences
Whether or not to replace multiple occurrences of the same dereference with a single symbol that cont...
std::size_t max_field_sensitivity_array_size
Maximum sizes for which field sensitivity will be applied to array cells.
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
bool show_symex_steps
Prints out the path that symex is actively taking during execution, includes diagnostic information a...
bool doing_path_exploration