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 
50 
53 
57 
65 
68  explicit symex_configt(const optionst &options);
69 };
70 
71 #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
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
symex_configt
Configuration used for a symbolic execution.
Definition: symex_config.h:17
optionst
Definition: options.h:23
symex_configt::cache_dereferences
bool cache_dereferences
Whether or not to replace multiple occurrences of the same dereference with a single symbol that cont...
Definition: symex_config.h:64
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:52
symex_configt::show_points_to_sets
bool show_points_to_sets
Definition: symex_config.h:49
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:56
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:33
symex_configt::debug_level
mp_integer debug_level
Definition: symex_config.h:39