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
	)

Definition at line 403 of file code_contracts.cpp.

Referenced by goto_instrument_parse_optionst::instrument_goto_program().