cprover
symex_config.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution Config
4 
5 Author: 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 
16 struct symex_configt final
17 {
21  unsigned max_depth;
22 
24 
26 
28 
30 
32 
34 
36 
38 
40 
45 
49 
52 
56 
59  explicit symex_configt(const optionst &options);
60 };
61 
62 #endif // CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H
symex_configt::havoc_undefined_functions
bool havoc_undefined_functions
Definition: symex_config.h:37
symex_configt::self_loops_to_assumptions
bool self_loops_to_assumptions
Definition: symex_config.h:29
symex_configt::partial_loops
bool partial_loops
Definition: symex_config.h:35
symex_configt
Configuration used for a symbolic execution.
Definition: symex_config.h:17
optionst
Definition: options.h:23
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
symex_configt::show_symex_steps
bool show_symex_steps
Prints out the path that symex is actively taking during execution, includes diagnostic information a...
Definition: symex_config.h:48
symex_configt::max_field_sensitivity_array_size
std::size_t max_field_sensitivity_array_size
Maximum sizes for which field sensitivity will be applied to array cells.
Definition: symex_config.h:51
symex_configt::doing_path_exploration
bool doing_path_exploration
Definition: symex_config.h:23
symex_configt::unwinding_assertions
bool unwinding_assertions
Definition: symex_config.h:33
symex_configt::allow_pointer_unsoundness
bool allow_pointer_unsoundness
Definition: symex_config.h:25
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
symex_configt::max_depth
unsigned max_depth
The maximum depth to take the execution to.
Definition: symex_config.h:21
symex_configt::complexity_limits_active
bool complexity_limits_active
Whether this run of symex is under complexity limits.
Definition: symex_config.h:55
symex_configt::constant_propagation
bool constant_propagation
Definition: symex_config.h:27
symex_configt::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
Definition: symex_config.h:44
symex_configt::symex_configt
symex_configt(const optionst &options)
Construct a symex_configt using options specified in an optionst.
Definition: symex_main.cpp:34
symex_configt::debug_level
mp_integer debug_level
Definition: symex_config.h:39