dynamic-frames Directory Reference

Directory dependency graph for dynamic-frames:

Files
	dfcc.cpp
	dfcc.h
	Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC)
	dfcc_cfg_info.cpp
	dfcc_cfg_info.h
	Class that computes CFG information about the loop structure of a GOTO function for the purpose of dynamic frame conditions checking and loop contract instrumentation.
	dfcc_check_loop_normal_form.cpp
	dfcc_check_loop_normal_form.h
	Checks normal form properties of natural loops in a GOTO program.
	dfcc_contract_clauses_codegen.cpp
	dfcc_contract_clauses_codegen.h
	Translates assigns and frees clauses of a function contract or loop contract into goto programs that build write sets or havoc write sets.
	dfcc_contract_functions.cpp
	dfcc_contract_functions.h
	Translates assigns and frees clauses of a function contract into goto functions that allow to build and havoc write sets dynamically.
	dfcc_contract_handler.cpp
	dfcc_contract_handler.h
	Specialisation of dfcc_contract_handlert for contracts.
	dfcc_contract_mode.cpp
	dfcc_contract_mode.h
	Enum type representing the contract checking and replacement modes.
	dfcc_infer_loop_assigns.cpp
	dfcc_infer_loop_assigns.h
	Infer a set of assigns clause targets for a natural loop.
	dfcc_instrument.cpp
	dfcc_instrument.h
	Add instrumentation to a goto program to perform frame condition checks.
	dfcc_instrument_loop.cpp
	dfcc_instrument_loop.h
	This class applies the loop contract transformation to a loop in a goto function.
	dfcc_is_cprover_symbol.cpp
	dfcc_is_cprover_symbol.h
	dfcc_is_freeable.cpp
	dfcc_is_freeable.h
	Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts.
	dfcc_is_fresh.cpp
	dfcc_is_fresh.h
	Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of contracts.
	dfcc_library.cpp
	dfcc_library.h
	Dynamic frame condition checking library loading.
	dfcc_lift_memory_predicates.cpp
	dfcc_lift_memory_predicates.h
	Collects all user-defined predicates that call functions is_fresh, pointer_in_range, obeys_contract and lifts them to function taking pointers by reference.
	dfcc_loop_nesting_graph.cpp
	dfcc_loop_nesting_graph.h
	Builds a graph describing how loops are nested in a GOTO program.
	dfcc_loop_tags.cpp
	dfcc_loop_tags.h
	Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head, body, exiting, latch.
	dfcc_obeys_contract.cpp
	dfcc_obeys_contract.h
	Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clauses of contracts.
	dfcc_pointer_equals.cpp
	dfcc_pointer_equals.h
	Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts.
	dfcc_pointer_in_range.cpp
	dfcc_pointer_in_range.h
	Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clauses of contracts.
	dfcc_root_object.cpp
	dfcc_root_object.h
	Utility functions that compute root object expressions for assigns clause targets and LHS expressions.
	dfcc_spec_functions.cpp
	dfcc_spec_functions.h
	Translate functions that specify assignable and freeable targets declaratively into active functions that build write sets dynamically by rewriting calls to front-end functions into calls to library functions defining their dynamic semantics.
	dfcc_swap_and_wrap.cpp
	dfcc_swap_and_wrap.h
	Given a function_id and contract_id, swaps its body to a function with a fresh mangled name, instruments it for dynamic frame condition checking, and replaces the original function's body with instructions encoding contract checking against the mangled function, or contract replacement.
	dfcc_utils.cpp
	dfcc_utils.h
	Dynamic frame condition checking utility functions.
	dfcc_wrapper_program.cpp
	dfcc_wrapper_program.h
	Generates the body of a wrapper function from a contract for contract checking or contract replacement.