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.

Member Function Documentation

◆ assign() [1/2]

◆ assign() [2/2]

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

Definition at line 86 of file path_symex_class.h.

References assign(), code_assignt::lhs(), and code_assignt::rhs().

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