cprover
code_contracts.cpp File Reference
+ Include dependency graph for code_contracts.cpp:

Go to the source code of this file.

Classes

class  code_contractst
 

Functions

static void check_apply_invariants (goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
 
void code_contracts (goto_modelt &goto_model)
 

Detailed Description

Verify and use annotated invariants and pre/post-conditions

Definition in file code_contracts.cpp.

Function Documentation

◆ check_apply_invariants()

static void check_apply_invariants ( goto_functionst::goto_functiont goto_function,
const local_may_aliast local_may_alias,
const goto_programt::targett  loop_head,
const loopt loop 
)
static

Definition at line 67 of file code_contracts.cpp.

◆ code_contracts()

void code_contracts ( goto_modelt goto_model)

Definition at line 412 of file code_contracts.cpp.