CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Macros | Functions | Variables

dfcc_library.cpp File Reference

#include "dfcc_library.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <goto-programs/goto_function.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/unwindset.h>
#include <ansi-c/c_expr.h>
#include <ansi-c/c_object_factory_parameters.h>
#include <ansi-c/cprover_library.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include <goto-instrument/generate_function_bodies.h>
#include <goto-instrument/unwind.h>
#include <linking/static_lifetime_init.h>
#include "dfcc_utils.h"

+ 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.

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

Creates the enum to type name mapping.

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

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

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

const std::set< irep_idt > create_assignable_builtin_names ()

static void add_checked_pragmas (source_locationt &sl)

Variables

static const std::set< dfcc_funt > to_inline

set of functions that need to be inlined

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.

static const std::set< dfcc_funt > fix_malloc_free_set

Set of functions that contain calls to assignable_malloc or assignable_free.

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 221 of file dfcc_library.cpp.

◆ create_assignable_builtin_names()

const std::set< irep_idt > create_assignable_builtin_names ( )

Definition at line 163 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 63 of file dfcc_library.cpp.

◆ create_dfcc_hook()

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

Definition at line 143 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 153 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:

= {

dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE,

dfcc_funt::IS_FRESH}

dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE

@ WRITE_SET_DEALLOCATE_FREEABLE

dfcc_funt::IS_FRESH

@ IS_FRESH

Set of functions that contain calls to assignable_malloc or assignable_free.

Definition at line 462 of file dfcc_library.cpp.

◆ to_inline

const std::set<dfcc_funt> to_inline

static

Initial value:

= {

dfcc_funt::WRITE_SET_CREATE,

dfcc_funt::WRITE_SET_RELEASE,

dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE,

dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE,

dfcc_funt::WRITE_SET_INSERT_OBJECT_FROM,

dfcc_funt::WRITE_SET_INSERT_OBJECT_UPTO,

dfcc_funt::WRITE_SET_ADD_FREEABLE,

dfcc_funt::WRITE_SET_ADD_ALLOCATED,

dfcc_funt::WRITE_SET_RECORD_DEAD,

dfcc_funt::WRITE_SET_RECORD_DEALLOCATED,

dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT,

dfcc_funt::WRITE_SET_CHECK_ARRAY_SET,

dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY,

dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE,

dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT,

dfcc_funt::WRITE_SET_CHECK_DEALLOCATE,

dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE}

dfcc_funt::WRITE_SET_INSERT_OBJECT_UPTO

@ WRITE_SET_INSERT_OBJECT_UPTO

dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT

@ WRITE_SET_CHECK_ASSIGNMENT

dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE

@ WRITE_SET_INSERT_ASSIGNABLE

dfcc_funt::WRITE_SET_RELEASE

@ WRITE_SET_RELEASE

dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE

@ WRITE_SET_INSERT_OBJECT_WHOLE

dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE

@ WRITE_SET_CHECK_ARRAY_REPLACE

dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT

@ WRITE_SET_CHECK_HAVOC_OBJECT

dfcc_funt::WRITE_SET_CHECK_DEALLOCATE

@ WRITE_SET_CHECK_DEALLOCATE

dfcc_funt::WRITE_SET_CHECK_ARRAY_SET

@ WRITE_SET_CHECK_ARRAY_SET

dfcc_funt::WRITE_SET_RECORD_DEAD

@ WRITE_SET_RECORD_DEAD

dfcc_funt::WRITE_SET_CREATE

@ WRITE_SET_CREATE

dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY

@ WRITE_SET_CHECK_ARRAY_COPY

dfcc_funt::WRITE_SET_ADD_FREEABLE

@ WRITE_SET_ADD_FREEABLE

dfcc_funt::WRITE_SET_RECORD_DEALLOCATED

@ WRITE_SET_RECORD_DEALLOCATED

dfcc_funt::WRITE_SET_ADD_ALLOCATED

@ WRITE_SET_ADD_ALLOCATED

dfcc_funt::WRITE_SET_INSERT_OBJECT_FROM

@ WRITE_SET_INSERT_OBJECT_FROM

set of functions that need to be inlined

Definition at line 391 of file dfcc_library.cpp.

◆ to_unwind

const std::map<dfcc_funt, int> to_unwind

static

Initial value:

= {

{dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT, 0},

{dfcc_funt::WRITE_SET_CHECK_ARRAY_SET, 0},

{dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY, 0},

{dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE, 0},

{dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT, 0},

{dfcc_funt::WRITE_SET_RECORD_DEALLOCATED, 0}}

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

Definition at line 425 of file dfcc_library.cpp.