cprover
Public Member Functions | Public Attributes | List of all members
symex_configt Struct Referencefinal

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...
 

Detailed Description

Configuration of the symbolic execution.

Definition at line 52 of file goto_symex.h.

Constructor & Destructor Documentation

◆ symex_configt()

symex_configt::symex_configt ( const optionst &  options)
explicit

Definition at line 26 of file symex_main.cpp.

Member Data Documentation

◆ allow_pointer_unsoundness

bool symex_configt::allow_pointer_unsoundness

Definition at line 56 of file goto_symex.h.

◆ constant_propagation

bool symex_configt::constant_propagation

Definition at line 57 of file goto_symex.h.

◆ debug_level

mp_integer symex_configt::debug_level

Definition at line 62 of file goto_symex.h.

◆ doing_path_exploration

bool symex_configt::doing_path_exploration

Definition at line 55 of file goto_symex.h.

◆ max_depth

unsigned symex_configt::max_depth

Definition at line 54 of file goto_symex.h.

◆ partial_loops

bool symex_configt::partial_loops

Definition at line 61 of file goto_symex.h.

◆ run_validation_checks

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.

◆ self_loops_to_assumptions

bool symex_configt::self_loops_to_assumptions

Definition at line 58 of file goto_symex.h.

◆ simplify_opt

bool symex_configt::simplify_opt

Definition at line 59 of file goto_symex.h.

◆ unwinding_assertions

bool symex_configt::unwinding_assertions

Definition at line 60 of file goto_symex.h.

The documentation for this struct was generated from the following files: