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