cprover
|
Verify and use annotated invariants and pre/post-conditions. More...
Go to the source code of this file.
Functions | |
void | code_contracts (symbol_tablet &symbol_table, goto_functionst &goto_functions) |
Verify and use annotated invariants and pre/post-conditions.
Definition in file code_contracts.h.
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().