cprover
|
Symbolic Execution of ANSI-C. More...
#include "goto_symex.h"
#include <cassert>
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <util/std_types.h>
#include <util/pointer_offset_size.h>
#include <util/symbol_table.h>
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/simplify_expr.h>
#include <util/prefix.h>
#include <util/string2int.h>
#include <util/c_types.h>
#include <linking/zero_initializer.h>
#include "goto_symex_state.h"
Go to the source code of this file.
Functions | |
static typet | c_sizeof_type_rec (const exprt &expr) |
irep_idt | get_symbol (const exprt &src) |
irep_idt | get_string_argument_rec (const exprt &src) |
irep_idt | get_string_argument (const exprt &src, const namespacet &ns) |
Symbolic Execution of ANSI-C.
Definition in file symex_builtin_functions.cpp.
Definition at line 33 of file symex_builtin_functions.cpp.
References irept::find(), forall_operands, irept::id(), irept::is_nil(), and irept::is_not_nil().
Referenced by goto_symext::symex_malloc().
irep_idt get_string_argument | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
Definition at line 280 of file symex_builtin_functions.cpp.
References get_string_argument_rec(), and simplify().
Referenced by goto_symext::symex_input(), goto_symext::symex_output(), and goto_symext::symex_printf().
Definition at line 254 of file symex_builtin_functions.cpp.
References irept::get_string(), irept::id(), exprt::is_zero(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by get_string_argument().
Definition at line 190 of file symex_builtin_functions.cpp.
References irept::get_bool(), ssa_exprt::get_object_name(), irept::id(), address_of_exprt::object(), typecast_exprt::op(), to_address_of_expr(), to_ssa_expr(), and to_typecast_expr().
Referenced by goto_symext::symex_gcc_builtin_va_arg_next().