contracts.h File Reference

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

#include <util/message.h>
#include <util/namespace.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>
#include <goto-instrument/loop_utils.h>
#include "loop_contract_config.h"
#include <map>
#include <set>
#include <string>
#include <unordered_set>

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    " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"
#define	FLAG_DISABLE_SIDE_EFFECT_CHECK    "disable-loop-contracts-side-effect-check"
#define	HELP_DISABLE_SIDE_EFFECT_CHECK
#define	FLAG_LOOP_CONTRACTS_NO_UNWIND   "loop-contracts-no-unwind"
#define	HELP_LOOP_CONTRACTS_NO_UNWIND    " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
#define	FLAG_LOOP_CONTRACTS_FILE   "loop-contracts-file"
#define	HELP_LOOP_CONTRACTS_FILE
#define	FLAG_REPLACE_CALL   "replace-call-with-contract"
#define	HELP_REPLACE_CALL
#define	FLAG_ENFORCE_CONTRACT   "enforce-contract"
#define	HELP_ENFORCE_CONTRACT

Detailed Description

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

Definition in file contracts.h.

Macro Definition Documentation

FLAG_DISABLE_SIDE_EFFECT_CHECK

#define FLAG_DISABLE_SIDE_EFFECT_CHECK    "disable-loop-contracts-side-effect-check"

Definition at line 36 of file contracts.h.

FLAG_ENFORCE_CONTRACT

#define FLAG_ENFORCE_CONTRACT   "enforce-contract"

Definition at line 55 of file contracts.h.

FLAG_LOOP_CONTRACTS

#define FLAG_LOOP_CONTRACTS   "apply-loop-contracts"

Definition at line 32 of file contracts.h.

FLAG_LOOP_CONTRACTS_FILE

#define FLAG_LOOP_CONTRACTS_FILE   "loop-contracts-file"

Definition at line 45 of file contracts.h.

FLAG_LOOP_CONTRACTS_NO_UNWIND

#define FLAG_LOOP_CONTRACTS_NO_UNWIND   "loop-contracts-no-unwind"

Definition at line 41 of file contracts.h.

FLAG_REPLACE_CALL

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

Definition at line 50 of file contracts.h.

HELP_DISABLE_SIDE_EFFECT_CHECK

#define HELP_DISABLE_SIDE_EFFECT_CHECK

Value:

  " {y--disable-loop-contracts-side-effect-check} \t UNSOUND OPTION.\t "       \
  " disable the check of side-effect of loop contracts\n"

Definition at line 38 of file contracts.h.

HELP_ENFORCE_CONTRACT

#define HELP_ENFORCE_CONTRACT

Value:

  " {y--enforce-contract} {ufunction}[/{ucontract}] \t "                       \
  "wrap function with an assertion of contract\n"

Definition at line 56 of file contracts.h.

HELP_LOOP_CONTRACTS

#define HELP_LOOP_CONTRACTS    " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"

Definition at line 33 of file contracts.h.

HELP_LOOP_CONTRACTS_FILE

#define HELP_LOOP_CONTRACTS_FILE

Value:

  " {y--loop-contracts-file} {ufile} \t "                                      \
  "parse and annotate loop contracts from files\n"

Definition at line 46 of file contracts.h.

HELP_LOOP_CONTRACTS_NO_UNWIND

#define HELP_LOOP_CONTRACTS_NO_UNWIND    " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"

Definition at line 42 of file contracts.h.

HELP_REPLACE_CALL

#define HELP_REPLACE_CALL

Value:

  " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t "             \
  "replace calls to {ufunction} with {ucontract}\n"

Definition at line 51 of file contracts.h.