CBMC
|
Symbolic Execution of ANSI-C. More...
#include "goto_symex.h"
#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/simplify_expr.h>
#include <util/std_code.h>
#include <util/string_constant.h>
#include "path_storage.h"
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 ¶meter, const pointer_typet &lhs_type, const namespacet &ns) |
Construct an entry for the var args array. More... | |
static irep_idt | get_string_argument_rec (const exprt &src) |
static irep_idt | get_string_argument (const exprt &src, 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. More... | |
Symbolic Execution of ANSI-C.
Definition in file symex_builtin_functions.cpp.
Definition at line 28 of file symex_builtin_functions.cpp.
|
static |
Definition at line 335 of file symex_builtin_functions.cpp.
Definition at line 304 of file symex_builtin_functions.cpp.
|
static |
Return an expression if operands
fulfills all criteria that we expect of the expression to be a variable argument list.
Definition at line 344 of file symex_builtin_functions.cpp.
|
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 213 of file symex_builtin_functions.cpp.