Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC) More...

#include <util/exception_utils.h>
#include <util/irep.h>
#include <util/message.h>
#include "dfcc_contract_clauses_codegen.h"
#include "dfcc_contract_handler.h"
#include "dfcc_instrument.h"
#include "dfcc_library.h"
#include "dfcc_lift_memory_predicates.h"
#include "dfcc_spec_functions.h"
#include "dfcc_swap_and_wrap.h"
#include <map>
#include <set>

Include dependency graph for dfcc.h:

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

Go to the source code of this file.

Classes
class	invalid_function_contract_pair_exceptiont
	Exception thrown for bad function/contract specification pairs passed on the CLI. More...

class	dfcct
	Entry point into the contracts transformation. More...

Macros
#define	FLAG_DFCC "dfcc"

#define	OPT_DFCC "(" FLAG_DFCC "):"

#define	HELP_DFCC

#define	FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"

#define	OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"

#define	HELP_ENFORCE_CONTRACT_REC

Functions
void	dfcc (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
	Applies function contracts transformation to GOTO model, using the dynamic frame condition checking approach. More...

Detailed Description

Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC)

All functions of the model are extended with a ghost parameter representing a dynamic frame and all their assignments are instrumented and checked against the dynamic frame parameter.

Targets specified by assigns clauses and frees clauses of the contracts are reified into dynamic data structures built by ghost code embedded in the program and are propagated through function calls and function pointer calls as ghost call arguments.

Definition in file dfcc.h.

Macro Definition Documentation

◆ FLAG_DFCC

#define FLAG_DFCC "dfcc"

Definition at line 54 of file dfcc.h.

◆ FLAG_ENFORCE_CONTRACT_REC

#define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"

Definition at line 62 of file dfcc.h.

◆ HELP_DFCC

#define HELP_DFCC

Value:

  " {y--dfcc} {uharness} \t "                                                  \
  "activate dynamic frame condition checking for contracts using the given "   \
  "harness as entry point\n"

Definition at line 57 of file dfcc.h.

◆ HELP_ENFORCE_CONTRACT_REC

#define HELP_ENFORCE_CONTRACT_REC

Value:

  " {y--enforce-contract-rec} {ufunction}[{y/}{ucontract}] \t "                \
  "wrap {ufunction} with an assertion of the contract and assume recursive "   \
  "calls to "                                                                  \
  "{ufunction} satisfy the contract\n"

Definition at line 64 of file dfcc.h.

◆ OPT_DFCC

#define OPT_DFCC "(" FLAG_DFCC "):"

Definition at line 55 of file dfcc.h.

◆ OPT_ENFORCE_CONTRACT_REC

#define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"

Definition at line 63 of file dfcc.h.

Classes

Macros

Functions