12 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H 13 #define CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H 26 std::list<path_symex_statet> &furter_states);
36 const goto_programt::instructiont &instruction=
50 std::list<path_symex_statet> &further_states);
55 std::list<path_symex_statet> &further_states)
64 const exprt &
function,
65 std::list<path_symex_statet> &further_states);
97 const exprt &ssa_rhs);
103 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H virtual void operator()(path_symex_statet &state, std::list< path_symex_statet > &furter_states)
void assign(path_symex_statet &state, const code_assignt &assignment)
void assign_rec(path_symex_statet &state, exprt::operandst &guard, const exprt &ssa_lhs, const exprt &ssa_rhs)
void symex_malloc(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
void function_call(path_symex_statet &state, const code_function_callt &call, std::list< path_symex_statet > &further_states)
void do_goto(path_symex_statet &state, bool taken)
virtual void do_assert_fail(path_symex_statet &state)
exprt read(const exprt &src)
void symex_va_arg_next(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
void assign(path_symex_statet &state, const exprt &lhs, const exprt &rhs)
void return_from_function(path_symex_statet &state)
std::vector< exprt > operandst
static bool propagate(const exprt &src)
goto_programt::const_targett get_instruction() const
Base class for all expressions.
Concrete Symbolic Transformer.
void function_call_rec(path_symex_statet &state, const code_function_callt &function_call, const exprt &function, std::list< path_symex_statet > &further_states)
void set_return_value(path_symex_statet &, const exprt &)
An expression containing a side effect.
path_symex_step_reft history