CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/symex_builtin_functions.cpp File Reference

CBMC

Loading...

Searching...

No Matches

symex_builtin_functions.cpp File Reference

Symbolic Execution of ANSI-C. More...

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/invariant_utils.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/std_code.h>
#include <util/string_constant.h>
#include "goto_symex.h"
#include "path_storage.h"
#include "simplify_expr_with_value_set.h"

+ Include dependency graph for symex_builtin_functions.cpp:

Go to the source code of this file.

Functions

static std::optional< typet > c_sizeof_type_rec (const exprt &expr)

static exprt va_list_entry (const irep_idt &parameter, const pointer_typet &lhs_type, const namespacet &ns)

Construct an entry for the var args array.

static irep_idt get_string_argument_rec (const exprt &src)

static irep_idt get_string_argument (const exprt &src, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)

static std::optional< exprt > get_va_args (const exprt::operandst &operands)

Return an expression if operands fulfills all criteria that we expect of the expression to be a variable argument list.

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file symex_builtin_functions.cpp.

Function Documentation

◆ c_sizeof_type_rec()

static std::optional< typet > c_sizeof_type_rec ( const exprt & expr )

inlinestatic

Definition at line 27 of file symex_builtin_functions.cpp.

◆ get_string_argument()

static irep_idt get_string_argument ( const exprt & src,

const value_sett & value_set,

const irep_idt & language_mode,

const namespacet & ns

)

static

Definition at line 336 of file symex_builtin_functions.cpp.

◆ get_string_argument_rec()

static irep_idt get_string_argument_rec ( const exprt & src )

static

Definition at line 305 of file symex_builtin_functions.cpp.

◆ get_va_args()

static std::optional< exprt > get_va_args ( const exprt::operandst & operands )

static

Return an expression if operands fulfills all criteria that we expect of the expression to be a variable argument list.

Definition at line 349 of file symex_builtin_functions.cpp.

◆ va_list_entry()

static exprt va_list_entry ( const irep_idt & parameter,

const pointer_typet & lhs_type,

const namespacet & ns

)

static

Construct an entry for the var args array.

Visual Studio complicates this as we need to put immediate values or pointers in there, depending on the size of the parameter.

Definition at line 214 of file symex_builtin_functions.cpp.