dfcc_library.h File Reference

Dynamic frame condition checking library loading. More...

#include <util/irep.h>
#include <util/message.h>
#include <goto-programs/goto_instruction_code.h>
#include <map>
#include <set>

Include dependency graph for dfcc_library.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	dfcc_libraryt
	Class interface to library types and functions defined in cprover_contracts.c. More...

Enumerations
enum class	dfcc_typet {   CAR , CAR_SET , CAR_SET_PTR , OBJ_SET ,   OBJ_SET_PTR , WRITE_SET , WRITE_SET_PTR }
	One enum value per type defined by the cprover_dfcc.c library file. More...
enum class	dfcc_funt {   CAR_CREATE , CAR_SET_CREATE , CAR_SET_INSERT , CAR_SET_REMOVE ,   CAR_SET_CONTAINS , OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID , OBJ_SET_CREATE_APPEND , OBJ_SET_RELEASE ,   OBJ_SET_ADD , OBJ_SET_APPEND , OBJ_SET_REMOVE , OBJ_SET_CONTAINS ,   OBJ_SET_CONTAINS_EXACT , WRITE_SET_CREATE , WRITE_SET_RELEASE , WRITE_SET_INSERT_ASSIGNABLE ,   WRITE_SET_INSERT_OBJECT_WHOLE , WRITE_SET_INSERT_OBJECT_FROM , WRITE_SET_INSERT_OBJECT_UPTO , WRITE_SET_ADD_FREEABLE ,   WRITE_SET_ADD_ALLOCATED , WRITE_SET_ADD_DECL , WRITE_SET_RECORD_DEAD , WRITE_SET_RECORD_DEALLOCATED ,   WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY , WRITE_SET_CHECK_ASSIGNMENT , WRITE_SET_CHECK_ARRAY_SET , WRITE_SET_CHECK_ARRAY_COPY ,   WRITE_SET_CHECK_ARRAY_REPLACE , WRITE_SET_CHECK_HAVOC_OBJECT , WRITE_SET_CHECK_DEALLOCATE , WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION ,   WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION , WRITE_SET_DEALLOCATE_FREEABLE , WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET , WRITE_SET_HAVOC_OBJECT_WHOLE ,   WRITE_SET_HAVOC_SLICE , LINK_IS_FRESH , LINK_ALLOCATED , LINK_DEALLOCATED ,   IS_FRESH , POINTER_IN_RANGE_DFCC , IS_FREEABLE , WAS_FREED ,   REPLACE_ENSURES_WAS_FREED_PRECONDITIONS , OBEYS_CONTRACT }
	One enum value per function defined by the cprover_dfcc.c library file. More...

Detailed Description

Dynamic frame condition checking library loading.

Definition in file dfcc_library.h.

Enumeration Type Documentation

dfcc_funt

enum dfcc_funt

strong

One enum value per function defined by the cprover_dfcc.c library file.

These enums are used to perform lookups into maps that contain the actual symbols and to avoid using strings/irep_ids everywhere.

Enumerator
CAR_CREATE	See also __CPROVER_contracts_car_create
CAR_SET_CREATE	See also __CPROVER_contracts_car_set_create
CAR_SET_INSERT	See also __CPROVER_contracts_car_set_insert
CAR_SET_REMOVE	See also __CPROVER_contracts_car_set_remove
CAR_SET_CONTAINS	See also __CPROVER_contracts_car_set_contains
OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID	See also __CPROVER_contracts_obj_set_create_indexed_by_object_id
OBJ_SET_CREATE_APPEND	See also __CPROVER_contracts_obj_set_create_append
OBJ_SET_RELEASE	See also __CPROVER_contracts_obj_set_release
OBJ_SET_ADD	See also __CPROVER_contracts_obj_set_add
OBJ_SET_APPEND	See also __CPROVER_contracts_obj_set_append
OBJ_SET_REMOVE	See also __CPROVER_contracts_obj_set_remove
OBJ_SET_CONTAINS	See also __CPROVER_contracts_obj_set_contains
OBJ_SET_CONTAINS_EXACT	See also __CPROVER_contracts_obj_set_contains_exact
WRITE_SET_CREATE	See also __CPROVER_contracts_write_set_create
WRITE_SET_RELEASE	See also __CPROVER_contracts_write_set_release
WRITE_SET_INSERT_ASSIGNABLE	See also __CPROVER_contracts_write_set_insert_assignable
WRITE_SET_INSERT_OBJECT_WHOLE	See also __CPROVER_contracts_write_set_insert_object_whole
WRITE_SET_INSERT_OBJECT_FROM	See also __CPROVER_contracts_write_set_insert_object_from
WRITE_SET_INSERT_OBJECT_UPTO	See also __CPROVER_contracts_write_set_object_upto
WRITE_SET_ADD_FREEABLE	See also __CPROVER_contracts_write_set_add_freeable
WRITE_SET_ADD_ALLOCATED	See also __CPROVER_contracts_write_set_add_allocated
WRITE_SET_ADD_DECL	See also __CPROVER_contracts_write_set_add_decl
WRITE_SET_RECORD_DEAD	See also __CPROVER_contracts_write_set_record_dead
WRITE_SET_RECORD_DEALLOCATED	See also __CPROVER_contracts_write_set_record_deallocated
WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY	See also __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty
WRITE_SET_CHECK_ASSIGNMENT	See also __CPROVER_contracts_write_set_check_assignment
WRITE_SET_CHECK_ARRAY_SET	See also __CPROVER_contracts_write_set_check_array_set
WRITE_SET_CHECK_ARRAY_COPY	See also __CPROVER_contracts_write_set_check_array_copy
WRITE_SET_CHECK_ARRAY_REPLACE	See also __CPROVER_contracts_write_set_check_array_replace
WRITE_SET_CHECK_HAVOC_OBJECT	See also __CPROVER_contracts_write_set_check_havoc_object
WRITE_SET_CHECK_DEALLOCATE	See also __CPROVER_contracts_write_set_check_deallocate
WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION	See also __CPROVER_contracts_write_set_check_assigns_clause_inclusion
WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION	See also __CPROVER_contracts_write_set_check_frees_clause_inclusion
WRITE_SET_DEALLOCATE_FREEABLE	See also __CPROVER_contracts_write_set_deallocate_freeable
WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET	See also __CPROVER_contracts_write_set_havoc_get_assignable_target
WRITE_SET_HAVOC_OBJECT_WHOLE	See also __CPROVER_contracts_write_set_havoc_object_whole
WRITE_SET_HAVOC_SLICE	See also __CPROVER_contracts_write_set_havoc_slice
LINK_IS_FRESH	See also __CPROVER_contracts_link_is_fresh
LINK_ALLOCATED	See also __CPROVER_contracts_link_allocated
LINK_DEALLOCATED	See also __CPROVER_contracts_link_deallocated
IS_FRESH	See also __CPROVER_contracts_is_fresh
POINTER_IN_RANGE_DFCC	See also __CPROVER_contracts_pointer_in_range_dfcc
IS_FREEABLE	See also __CPROVER_contracts_is_freeable
WAS_FREED	See also __CPROVER_contracts_was_freed
REPLACE_ENSURES_WAS_FREED_PRECONDITIONS	See also __CPROVER_contracts_check_replace_ensures_was_freed_preconditions
OBEYS_CONTRACT	See also __CPROVER_contracts_obeys_contract

Definition at line 47 of file dfcc_library.h.

dfcc_typet

enum dfcc_typet

strong

One enum value per type defined by the cprover_dfcc.c library file.

These enums are used to perform lookups into maps that contain the actual symbols and to avoid using strings/irep_ids everywhere.

Enumerator
CAR	type of descriptors of conditionally assignable ranges of bytes
CAR_SET	type of sets of CAR
CAR_SET_PTR	type of pointers to sets of CAR
OBJ_SET	type of sets of object identifiers
OBJ_SET_PTR	type of pointers to sets of object identifiers
WRITE_SET	type of descriptors of assignable/freeable sets of locations
WRITE_SET_PTR	type of pointers to descriptors of assignable/freeable sets of locations

Definition at line 26 of file dfcc_library.h.