cprover
Loading...
Searching...
No Matches
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
16struct 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
BigInt mp_integer
Definition: smt_terms.h:12
Configuration used for a symbolic execution.
Definition: symex_config.h:17
bool partial_loops
Definition: symex_config.h:35
mp_integer debug_level
Definition: symex_config.h:39
bool complexity_limits_active
Whether this run of symex is under complexity limits.
Definition: symex_config.h:56
bool unwinding_assertions
Definition: symex_config.h:33
bool show_points_to_sets
Definition: symex_config.h:49
bool allow_pointer_unsoundness
Definition: symex_config.h:25
bool constant_propagation
Definition: symex_config.h:27
bool havoc_undefined_functions
Definition: symex_config.h:37
unsigned max_depth
The maximum depth to take the execution to.
Definition: symex_config.h:21
bool self_loops_to_assumptions
Definition: symex_config.h:29
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
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
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
bool show_symex_steps
Prints out the path that symex is actively taking during execution, includes diagnostic information a...
Definition: symex_config.h:48
bool doing_path_exploration
Definition: symex_config.h:23