contracts.h File Reference

#include <goto-programs/goto_functions.h>
#include <goto-programs/frame_enforcer.h>
#include <util/symtab/context.h>
#include <util/symtab/namespace.h>
#include <functional>
#include <map>
#include <set>
#include <string>

Include dependency graph for contracts.h:

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

Go to the source code of this file.

Classes
class	code_contractst
	Basic contract handling class Provides contract checking and replacement functionality at goto function level. More...
struct	code_contractst::is_fresh_mapping_t
	Structure to store is_fresh mapping information. More...
struct	code_contractst::ptr_field_snapshot_t
	Per-field snapshot for pointer-struct-field assigns compliance. More...
struct	code_contractst::ptr_deref_snapshot_t
	Snapshot for pointer-parameter dereference assigns compliance (Phase 2C). More...
struct	code_contractst::arr_elem_snapshot_t
	Snapshot for array element assigns compliance (Phase 2B). More...
struct	code_contractst::param_extentt
	Byte extent of a harness-allocated pointer parameter. More...