CBMC
|
Specialisation of dfcc_contract_handlert for contracts. More...
#include <ansi-c/goto-conversion/goto_convert_class.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include "dfcc_contract_functions.h"
#include <set>
Go to the source code of this file.
Classes | |
class | dfcc_contract_handlert |
A contract is represented by a function declaration or definition with contract clauses attached to its signature: More... | |
Specialisation of dfcc_contract_handlert for contracts.
Definition in file dfcc_contract_handler.h.