cprover
|
Concrete Symbolic Transformer. More...
#include "path_symex.h"
#include <util/arith_tools.h>
#include <util/simplify_expr.h>
#include <util/string2int.h>
#include <util/byte_operators.h>
#include <util/pointer_offset_size.h>
#include <util/base_type.h>
#include <util/prefix.h>
#include <util/c_types.h>
#include <linking/zero_initializer.h>
#include <pointer-analysis/dereference.h>
#include "path_symex_class.h"
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) |
Concrete Symbolic Transformer.
Definition in file path_symex.cpp.
Definition at line 135 of file path_symex.cpp.
References irept::find(), forall_operands, irept::id(), irept::is_nil(), and irept::is_not_nil().
Referenced by path_symext::symex_malloc().
|
static |
Definition at line 271 of file path_symex.cpp.
References symbol_exprt::get_identifier(), irept::id(), address_of_exprt::object(), typecast_exprt::op(), to_address_of_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by path_symext::symex_va_arg_next().
void path_symex | ( | path_symex_statet & | state, |
std::list< path_symex_statet > & | further_states | ||
) |
Definition at line 1113 of file path_symex.cpp.
References path_symex().
Referenced by path_searcht::operator()(), path_symex(), path_symex_assert_fail(), and path_symex_goto().
void path_symex | ( | path_symex_statet & | state | ) |
Definition at line 1121 of file path_symex.cpp.
References path_symex().
void path_symex_assert_fail | ( | path_symex_statet & | state | ) |
Definition at line 1135 of file path_symex.cpp.
References path_symex().
void path_symex_goto | ( | path_symex_statet & | state, |
bool | taken | ||
) |
Definition at line 1127 of file path_symex.cpp.
References path_symex().