cprover
path_symext Class Reference

#include <path_symex_class.h>

Public Types

typedef path_symex_stept stept
 

Public Member Functions

 path_symext ()
 
virtual void operator() (path_symex_statet &state, std::list< path_symex_statet > &furter_states)
 
virtual void operator() (path_symex_statet &state)
 
void do_goto (path_symex_statet &state, bool taken)
 
virtual void do_assert_fail (path_symex_statet &state)
 

Protected Member Functions

void do_goto (path_symex_statet &state, std::list< path_symex_statet > &further_states)
 
void function_call (path_symex_statet &state, const code_function_callt &call, std::list< path_symex_statet > &further_states)
 
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 return_from_function (path_symex_statet &state)
 
void set_return_value (path_symex_statet &, const exprt &)
 
void symex_malloc (path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
 
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 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)
 

Static Protected Member Functions

static bool propagate (const exprt &src)
 

Detailed Description

Definition at line 17 of file path_symex_class.h.

Member Typedef Documentation

§ stept

Definition at line 45 of file path_symex_class.h.

Constructor & Destructor Documentation

§ path_symext()

path_symext::path_symext ( )
inline

Definition at line 20 of file path_symex_class.h.

References do_goto(), and operator()().

Member Function Documentation

§ assign() [1/2]

§ assign() [2/2]

void path_symext::assign ( path_symex_statet state,
const code_assignt assignment 
)
inlineprotected

§ assign_rec()

§ do_assert_fail()

§ do_goto() [1/2]

§ do_goto() [2/2]

§ function_call()

void path_symext::function_call ( path_symex_statet state,
const code_function_callt call,
std::list< path_symex_statet > &  further_states 
)
inlineprotected

§ function_call_rec()

§ operator()() [1/2]

§ operator()() [2/2]

void path_symext::operator() ( path_symex_statet state)
virtual

Definition at line 1105 of file path_symex.cpp.

References operator()().

§ propagate()

§ return_from_function()

§ set_return_value()

void path_symext::set_return_value ( path_symex_statet state,
const exprt v 
)
protected

§ symex_malloc()

§ symex_va_arg_next()


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