cprover
code_contracts.h File Reference

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

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

Go to the source code of this file.

Functions

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.h.

Function Documentation

§ code_contracts()

void code_contracts ( symbol_tablet symbol_table,
goto_functionst goto_functions 
)