dfcc_library.h File Reference

Dynamic frame condition checking library loading. More...

#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 , PTR_PRED_CTX ,   PTR_PRED_CTX_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 ,   PTR_PRED_CTX_INIT , PTR_PRED_CTX_RESET , 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_PTR_PRED_CTX ,   LINK_ALLOCATED , LINK_DEALLOCATED , POINTER_EQUALS , 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 class 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
PTR_PRED_CTX_INIT	See also __CPROVER_contracts_ptr_pred_ctx_init
PTR_PRED_CTX_RESET	See also __CPROVER_contracts_ptr_pred_ctx_reset
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_PTR_PRED_CTX	See also __CPROVER_contracts_link_ptr_pred_ctx
LINK_ALLOCATED	See also __CPROVER_contracts_link_allocated
LINK_DEALLOCATED	See also __CPROVER_contracts_link_deallocated
POINTER_EQUALS	See also __CPROVER_contracts_pointer_equals
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 50 of file dfcc_library.h.

dfcc_typet

enum class 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
PTR_PRED_CTX	type of context info for pointer predicates evaluation
PTR_PRED_CTX_PTR	type of pointers to context info for pointer predicates evaluation
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 25 of file dfcc_library.h.