cprover
|
Configuration of the symbolic execution. More...
#include <goto_symex.h>
Public Member Functions | |
symex_configt (const optionst &options) | |
Public Attributes | |
unsigned | max_depth |
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 |
mp_integer | debug_level |
bool | run_validation_checks |
Should the additional validation checks be run? More... | |
Configuration of the symbolic execution.
Definition at line 52 of file goto_symex.h.
|
explicit |
Definition at line 26 of file symex_main.cpp.
bool symex_configt::allow_pointer_unsoundness |
Definition at line 56 of file goto_symex.h.
bool symex_configt::constant_propagation |
Definition at line 57 of file goto_symex.h.
mp_integer symex_configt::debug_level |
Definition at line 62 of file goto_symex.h.
bool symex_configt::doing_path_exploration |
Definition at line 55 of file goto_symex.h.
unsigned symex_configt::max_depth |
Definition at line 54 of file goto_symex.h.
bool symex_configt::partial_loops |
Definition at line 61 of file goto_symex.h.
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 68 of file goto_symex.h.
bool symex_configt::self_loops_to_assumptions |
Definition at line 58 of file goto_symex.h.
bool symex_configt::simplify_opt |
Definition at line 59 of file goto_symex.h.
bool symex_configt::unwinding_assertions |
Definition at line 60 of file goto_symex.h.