CBMC
Functions
c_typecheck_shadow_memory_builtin.cpp File Reference
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/expr.h>
#include <util/string_constant.h>
#include "c_typecheck_base.h"
#include "expr2c.h"
+ Include dependency graph for c_typecheck_shadow_memory_builtin.cpp:

Go to the source code of this file.

Functions

static symbol_exprt typecheck_field_decl (const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
 Function to typecheck a shadow memory field_declaration function. More...
 
static symbol_exprt typecheck_get_field (const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
 Function to typecheck a shadow memory get_field function. More...
 
static symbol_exprt typecheck_set_field (const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
 Function to typecheck a shadow memory set_field function. More...
 

Function Documentation

◆ typecheck_field_decl()

static symbol_exprt typecheck_field_decl ( const side_effect_expr_function_callt &  expr,
const irep_idt &  identifier,
const namespacet &  ns 
)
static

Function to typecheck a shadow memory field_declaration function.

Returns
a symbol of the shadow memory function
Exceptions
invalid_source_file_exceptiontif the typecheck fails.

Definition at line 17 of file c_typecheck_shadow_memory_builtin.cpp.

◆ typecheck_get_field()

static symbol_exprt typecheck_get_field ( const side_effect_expr_function_callt &  expr,
const irep_idt &  identifier,
const namespacet &  ns 
)
static

Function to typecheck a shadow memory get_field function.

Returns
a symbol of the shadow memory function.
Exceptions
invalid_source_file_exceptiontif the typecheck fails.

Definition at line 82 of file c_typecheck_shadow_memory_builtin.cpp.

◆ typecheck_set_field()

static symbol_exprt typecheck_set_field ( const side_effect_expr_function_callt &  expr,
const irep_idt &  identifier,
const namespacet &  ns 
)
static

Function to typecheck a shadow memory set_field function.

Returns
a symbol of the shadow memory function.
Exceptions
invalid_source_file_exceptiontif the typecheck fails.

Definition at line 147 of file c_typecheck_shadow_memory_builtin.cpp.