cprover
symex_builtin_functions.cpp File Reference

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

◆ get_string_argument()

irep_idt get_string_argument ( const exprt src,
const namespacet ns 
)

◆ get_string_argument_rec()

irep_idt get_string_argument_rec ( const exprt src)

◆ get_symbol()