cprover
code_contracts.h File Reference
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void code_contracts (goto_modelt &)
 

Detailed Description

Verify and use annotated invariants and pre/post-conditions

Definition in file code_contracts.h.

Function Documentation

◆ code_contracts()

void code_contracts ( goto_modelt )

Definition at line 412 of file code_contracts.cpp.