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