cprover: goto-symex/symex_builtin_functions.cpp File Reference

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"

Include dependency graph for symex_builtin_functions.cpp:

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)

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file symex_builtin_functions.cpp.

Function Documentation

◆ c_sizeof_type_rec()

static typet c_sizeof_type_rec ( const exprt & expr )

inlinestatic

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().

◆ get_string_argument()

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().

◆ get_string_argument_rec()

irep_idt get_string_argument_rec ( const exprt & src )

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().

◆ get_symbol()

irep_idt get_symbol ( const exprt & src )

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().