dynamic-frames Directory Reference

Directory dependency graph for dynamic-frames:

Files
file	dfcc.cpp [code]
file	dfcc.h [code]
	Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC)
file	dfcc_cfg_info.cpp [code]
file	dfcc_cfg_info.h [code]
	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.
file	dfcc_check_loop_normal_form.cpp [code]
file	dfcc_check_loop_normal_form.h [code]
	Checks normal form properties of natural loops in a GOTO program.
file	dfcc_contract_clauses_codegen.cpp [code]
file	dfcc_contract_clauses_codegen.h [code]
	Translates assigns and frees clauses of a function contract or loop contract into goto programs that build write sets or havoc write sets.
file	dfcc_contract_functions.cpp [code]
file	dfcc_contract_functions.h [code]
	Translates assigns and frees clauses of a function contract into goto functions that allow to build and havoc write sets dynamically.
file	dfcc_contract_handler.cpp [code]
file	dfcc_contract_handler.h [code]
	Specialisation of dfcc_contract_handlert for contracts.
file	dfcc_contract_mode.cpp [code]
file	dfcc_contract_mode.h [code]
	Enum type representing the contract checking and replacement modes.
file	dfcc_infer_loop_assigns.cpp [code]
file	dfcc_infer_loop_assigns.h [code]
	Infer a set of assigns clause targets for a natural loop.
file	dfcc_instrument.cpp [code]
file	dfcc_instrument.h [code]
	Add instrumentation to a goto program to perform frame condition checks.
file	dfcc_instrument_loop.cpp [code]
file	dfcc_instrument_loop.h [code]
	This class applies the loop contract transformation to a loop in a goto function.
file	dfcc_is_cprover_symbol.cpp [code]
file	dfcc_is_cprover_symbol.h [code]
file	dfcc_is_freeable.cpp [code]
file	dfcc_is_freeable.h [code]
	Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts.
file	dfcc_is_fresh.cpp [code]
file	dfcc_is_fresh.h [code]
	Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of contracts.
file	dfcc_library.cpp [code]
file	dfcc_library.h [code]
	Dynamic frame condition checking library loading.
file	dfcc_lift_memory_predicates.cpp [code]
file	dfcc_lift_memory_predicates.h [code]
	Collects all user-defined predicates that call functions is_fresh, pointer_in_range, obeys_contract and lifts them to function taking pointers by reference.
file	dfcc_loop_nesting_graph.cpp [code]
file	dfcc_loop_nesting_graph.h [code]
	Builds a graph describing how loops are nested in a GOTO program.
file	dfcc_loop_tags.cpp [code]
file	dfcc_loop_tags.h [code]
	Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head, body, exiting, latch.
file	dfcc_obeys_contract.cpp [code]
file	dfcc_obeys_contract.h [code]
	Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clauses of contracts.
file	dfcc_pointer_in_range.cpp [code]
file	dfcc_pointer_in_range.h [code]
	Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clauses of contracts.
file	dfcc_root_object.cpp [code]
file	dfcc_root_object.h [code]
	Utility functions that compute root object expressions for assigns clause targets and LHS expressions.
file	dfcc_spec_functions.cpp [code]
file	dfcc_spec_functions.h [code]
	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.
file	dfcc_swap_and_wrap.cpp [code]
file	dfcc_swap_and_wrap.h [code]
	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.
file	dfcc_utils.cpp [code]
file	dfcc_utils.h [code]
	Dynamic frame condition checking utility functions.
file	dfcc_wrapper_program.cpp [code]
file	dfcc_wrapper_program.h [code]
	Generates the body of a wrapper function from a contract for contract checking or contract replacement.