cprover
code_contracts.cpp File Reference

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

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 (symbol_tablet &symbol_table, goto_functionst &goto_functions)
 

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

§ code_contracts()

void code_contracts ( symbol_tablet symbol_table,
goto_functionst goto_functions 
)