Verify and use annotated invariants and pre/post-conditions. More...

#include <map>
#include <set>
#include <string>
#include <unordered_set>
#include <goto-instrument/loop_utils.h>
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/instrument_preconditions.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/optional.h>
#include <util/pointer_expr.h>

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

Macros
#define	FLAG_LOOP_CONTRACTS "apply-loop-contracts"

#define	HELP_LOOP_CONTRACTS

#define	FLAG_REPLACE_CALL "replace-call-with-contract"

#define	HELP_REPLACE_CALL

#define	FLAG_ENFORCE_CONTRACT "enforce-contract"

#define	HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n"

Detailed Description

Verify and use annotated invariants and pre/post-conditions.

Definition in file contracts.h.

Macro Definition Documentation

◆ FLAG_ENFORCE_CONTRACT

#define FLAG_ENFORCE_CONTRACT "enforce-contract"

Definition at line 44 of file contracts.h.

◆ FLAG_LOOP_CONTRACTS

#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"

Definition at line 34 of file contracts.h.

◆ FLAG_REPLACE_CALL

#define FLAG_REPLACE_CALL "replace-call-with-contract"

Definition at line 39 of file contracts.h.

◆ HELP_ENFORCE_CONTRACT

#define HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n"

Definition at line 45 of file contracts.h.

◆ HELP_LOOP_CONTRACTS

#define HELP_LOOP_CONTRACTS

Value:

" --apply-loop-contracts\n" \

" check and use loop contracts when provided\n"

Definition at line 35 of file contracts.h.

◆ HELP_REPLACE_CALL

#define HELP_REPLACE_CALL

Value:

" --replace-call-with-contract <fun>\n" \

" replace calls to fun with fun's contract\n"

Definition at line 40 of file contracts.h.

Classes

Macros