builtin_functions.cpp File Reference

#include "irep2/irep2_utils.h"
#include <ac_config.h>
#include <cassert>
#include <functional>
#include <goto-programs/destructor.h>
#include <goto-programs/goto_convert_class.h>
#include <regex>
#include <util/arith/arith_tools.h>
#include <util/base/filesystem.h>
#include <util/lang/c_types.h>
#include <util/symtab/cprover_prefix.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/irep/location.h>
#include <util/message/message.h>
#include <util/message/format.h>
#include <util/base/prefix.h>
#include <util/irep/std_code.h>
#include <util/irep/std_expr.h>
#include <util/expr/string_constant.h>
#include <util/expr/type_byte_size.h>

Include dependency graph for builtin_functions.cpp:

Functions
static void	simplify_via_irep2 (exprt &e)
static void	get_string_constant (const exprt &expr, std::string &the_string)
static typet	sizeof_measured_type (const exprt &src)
static void	get_alloc_type_rec (const exprt &src, typet &type, exprt &size, bool is_mul=false)
static void	get_alloc_type (const exprt &src, typet &type, exprt &size)
static exprt *	find_cpp_new_constructor (exprt &e)
static bool	array_leaves (const namespacet &ns, const typet &type, typet &leaf, BigInt &n)
static std::size_t	list_size (const exprt &init)
static exprt	list_element (const exprt &init, std::size_t i)
static bool	is_splittable_list (const namespacet &ns, const exprt &init)
static exprt *	element_constructor (exprt &init)
bool	is_lvalue (const exprt &expr)
exprt	make_va_list (const exprt &expr)
static void	emit_va_marker_call (const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
static exprt	assigns_marker_operand (const exprt &target)
static bool	is_alloca_function (const std::string &base_name)
	__ESBMC_alloca is the models' spelling: its temp is not a return_value$_alloca$/___builtin_alloca$ name, so its storage never expires (#8691).

Function Documentation

array_leaves()

bool array_leaves ( const namespacet & ns, const typet & type, typet & leaf, BigInt & n )

static

assigns_marker_operand()

exprt assigns_marker_operand ( const exprt & target )

static

element_constructor()

exprt * element_constructor ( exprt & init )

static

emit_va_marker_call()

void emit_va_marker_call ( const exprt & function, const exprt::operandst & arguments, goto_programt & dest )

static

find_cpp_new_constructor()

exprt * find_cpp_new_constructor ( exprt & e )

static

get_alloc_type()

void get_alloc_type ( const exprt & src, typet & type, exprt & size )

static

get_alloc_type_rec()

void get_alloc_type_rec ( const exprt & src, typet & type, exprt & size, bool is_mul = false )

static

get_string_constant()

void get_string_constant ( const exprt & expr, std::string & the_string )

static

is_alloca_function()

bool is_alloca_function ( const std::string & base_name )

static

__ESBMC_alloca is the models' spelling: its temp is not a return_value$_alloca$/___builtin_alloca$ name, so its storage never expires (#8691).

is_lvalue()

bool is_lvalue

(

const exprt &

expr

)

is_splittable_list()

bool is_splittable_list ( const namespacet & ns, const exprt & init )

static

list_element()

exprt list_element ( const exprt & init, std::size_t i )

static

list_size()

std::size_t list_size ( const exprt & init )

static

make_va_list()

exprt make_va_list

(

const exprt &

expr

)

simplify_via_irep2()

void simplify_via_irep2 ( exprt & e )

static

sizeof_measured_type()

typet sizeof_measured_type ( const exprt & src )

static