CBMC
contracts.cpp File Reference

Verify and use annotated loop and function contracts. More...

+ Include dependency graph for contracts.cpp:

Go to the source code of this file.

Functions

static void throw_on_unsupported (const goto_programt &program)
 Throws an exception if a contract uses unsupported constructs like: More...
 
static void generate_contract_constraints (symbol_tablet &symbol_table, goto_convertt &converter, exprt &instantiated_clause, const irep_idt &mode, const std::function< void(goto_programt &)> &is_fresh_update, goto_programt &program, const source_locationt &location)
 This function generates instructions for all contract constraint, i.e., assumptions and assertions based on requires and ensures clauses. More...
 
static const code_with_contract_typetget_contract (const irep_idt &function, const namespacet &ns)
 

Detailed Description

Verify and use annotated loop and function contracts.

Definition in file contracts.cpp.

Function Documentation

◆ generate_contract_constraints()

static void generate_contract_constraints ( symbol_tablet symbol_table,
goto_convertt converter,
exprt instantiated_clause,
const irep_idt mode,
const std::function< void(goto_programt &)> &  is_fresh_update,
goto_programt program,
const source_locationt location 
)
static

This function generates instructions for all contract constraint, i.e., assumptions and assertions based on requires and ensures clauses.

Definition at line 561 of file contracts.cpp.

◆ get_contract()

static const code_with_contract_typet& get_contract ( const irep_idt function,
const namespacet ns 
)
static

Definition at line 589 of file contracts.cpp.

◆ throw_on_unsupported()

static void throw_on_unsupported ( const goto_programt program)
static

Throws an exception if a contract uses unsupported constructs like:

  • obeys_contract predicates

Definition at line 543 of file contracts.cpp.