CBMC
dfcc_library.cpp File Reference
+ Include dependency graph for dfcc_library.cpp:

Go to the source code of this file.

Macros

#define CONTRACTS_PREFIX   CPROVER_PREFIX "contracts_"
 

Functions

template<typename K , typename V >
std::map< V, K > swap_map (std::map< K, V > const &map)
 Swaps keys and values in a map. More...
 
const std::map< dfcc_typet, irep_idtcreate_dfcc_type_to_name ()
 Creates the enum to type name mapping. More...
 
const std::map< dfcc_funt, irep_idtcreate_dfcc_fun_to_name ()
 
const std::map< irep_idt, dfcc_funtcreate_dfcc_hook ()
 
const std::map< irep_idt, dfcc_funtcreate_havoc_hook ()
 
const std::set< irep_idtcreate_assignable_builtin_names ()
 
static void add_checked_pragmas (source_locationt &sl)
 

Variables

static const std::set< dfcc_funtto_inline
 set of functions that need to be inlined More...
 
static const std::map< dfcc_funt, int > to_unwind
 set of functions that need to be unwound to assigns clause size with corresponding loop identifiers. More...
 
static const std::set< dfcc_funtfix_malloc_free_set
 Set of functions that contain calls to assignable_malloc or assignable_free. More...
 

Macro Definition Documentation

◆ CONTRACTS_PREFIX

#define CONTRACTS_PREFIX   CPROVER_PREFIX "contracts_"

Definition at line 46 of file dfcc_library.cpp.

Function Documentation

◆ add_checked_pragmas()

static void add_checked_pragmas ( source_locationt sl)
static

Definition at line 216 of file dfcc_library.cpp.

◆ create_assignable_builtin_names()

const std::set<irep_idt> create_assignable_builtin_names ( )

Definition at line 158 of file dfcc_library.cpp.

◆ create_dfcc_fun_to_name()

const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name ( )

Definition at line 61 of file dfcc_library.cpp.

◆ create_dfcc_hook()

const std::map<irep_idt, dfcc_funt> create_dfcc_hook ( )

Definition at line 138 of file dfcc_library.cpp.

◆ create_dfcc_type_to_name()

const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name ( )

Creates the enum to type name mapping.

Definition at line 49 of file dfcc_library.cpp.

◆ create_havoc_hook()

const std::map<irep_idt, dfcc_funt> create_havoc_hook ( )

Definition at line 148 of file dfcc_library.cpp.

◆ swap_map()

template<typename K , typename V >
std::map<V, K> swap_map ( std::map< K, V > const &  map)

Swaps keys and values in a map.

Definition at line 37 of file dfcc_library.cpp.

Variable Documentation

◆ fix_malloc_free_set

const std::set<dfcc_funt> fix_malloc_free_set
static
Initial value:

Set of functions that contain calls to assignable_malloc or assignable_free.

Definition at line 457 of file dfcc_library.cpp.

◆ to_inline

const std::set<dfcc_funt> to_inline
static
Initial value:
= {
@ WRITE_SET_INSERT_OBJECT_UPTO
@ WRITE_SET_CHECK_ASSIGNMENT
@ WRITE_SET_INSERT_ASSIGNABLE
@ WRITE_SET_RELEASE
@ WRITE_SET_INSERT_OBJECT_WHOLE
@ WRITE_SET_CHECK_ARRAY_REPLACE
@ WRITE_SET_CHECK_HAVOC_OBJECT
@ WRITE_SET_CHECK_DEALLOCATE
@ WRITE_SET_CHECK_ARRAY_SET
@ WRITE_SET_RECORD_DEAD
@ WRITE_SET_CREATE
@ WRITE_SET_CHECK_ARRAY_COPY
@ WRITE_SET_ADD_FREEABLE
@ WRITE_SET_RECORD_DEALLOCATED
@ WRITE_SET_ADD_ALLOCATED
@ WRITE_SET_INSERT_OBJECT_FROM

set of functions that need to be inlined

Definition at line 386 of file dfcc_library.cpp.

◆ to_unwind

const std::map<dfcc_funt, int> to_unwind
static
Initial value:

set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.

Definition at line 420 of file dfcc_library.cpp.