12 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H 13 #define CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H 45 return index==std::numeric_limits<std::size_t>::max();
64 void build_history(std::vector<path_symex_step_reft> &dest)
const;
87 return branch==BRANCH_TAKEN;
92 return branch==BRANCH_NOT_TAKEN;
97 return branch==BRANCH_TAKEN || branch==BRANCH_NOT_TAKEN;
126 void output(std::ostream &)
const;
153 step_container.clear();
169 *
this=
get().predecessor;
181 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
decision_proceduret & operator<<(decision_proceduret &dest, path_symex_step_reft src)
void build_history(std::vector< path_symex_step_reft > &dest) const
path_symex_step_reft & operator--()
path_symex_stept & get() const
void convert(decision_proceduret &dest) const
path_symex_historyt & get_history() const
path_symex_step_reft(class path_symex_historyt &_history)
path_symex_step_reft predecessor
void generate_successor()
API to expression classes.
std::vector< path_symex_stept > step_containert
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
step_containert step_container
class path_symex_historyt * history
void branch(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Base class for all expressions.
path_symex_stept & operator*() const
bool is_branch_not_taken() const
path_symex_stept * operator->() const
Expression to hold a symbol (variable)
bool is_branch_taken() const
Generic exception types primarily designed for use with invariants.