symex_config.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution Config
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H
#define CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H
 
class optionst;
 
struct symex_configt final
{
  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;
 
  bool havoc_undefined_functions;
 
  bool run_validation_checks;
 
  bool show_symex_steps;
  bool show_points_to_sets;
 
  std::size_t max_field_sensitivity_array_size;
 
  bool complexity_limits_active;
 
  bool cache_dereferences;
 
  explicit symex_configt(const optionst &options);
};
 
#endif // CPROVER_GOTO_SYMEX_SYMEX_CONFIG_H