cprover
path_symex.cpp File Reference

Concrete Symbolic Transformer. More...

Include dependency graph for path_symex.cpp:

Go to the source code of this file.

Functions

static typet c_sizeof_type_rec (const exprt &expr)
 
static irep_idt get_old_va_symbol (const path_symex_statet &state, const exprt &src)
 
void path_symex (path_symex_statet &state, std::list< path_symex_statet > &further_states)
 
void path_symex (path_symex_statet &state)
 
void path_symex_goto (path_symex_statet &state, bool taken)
 
void path_symex_assert_fail (path_symex_statet &state)
 

Detailed Description

Concrete Symbolic Transformer.

Definition in file path_symex.cpp.

Function Documentation

◆ c_sizeof_type_rec()

static typet c_sizeof_type_rec ( const exprt expr)
inlinestatic

◆ get_old_va_symbol()

static irep_idt get_old_va_symbol ( const path_symex_statet state,
const exprt src 
)
static

◆ path_symex() [1/2]

void path_symex ( path_symex_statet state,
std::list< path_symex_statet > &  further_states 
)

◆ path_symex() [2/2]

void path_symex ( path_symex_statet state)

Definition at line 1121 of file path_symex.cpp.

References path_symex().

◆ path_symex_assert_fail()

void path_symex_assert_fail ( path_symex_statet state)

Definition at line 1135 of file path_symex.cpp.

References path_symex().

◆ path_symex_goto()

void path_symex_goto ( path_symex_statet state,
bool  taken 
)

Definition at line 1127 of file path_symex.cpp.

References path_symex().