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 <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 <goto-instrument/unwindset.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. More...
const std::map< dfcc_typet, irep_idt >	create_dfcc_type_to_name ()
	Creates the enum to type name mapping. More...
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 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_funt >	fix_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:

= {
  dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE,
  dfcc_funt::IS_FRESH}

Set of functions that contain calls to assignable_malloc or assignable_free.

Definition at line 456 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}

set of functions that need to be inlined

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