Verify and use annotated invariants and pre/post-conditions. More...
#include "code_contracts.h"#include <util/expr_util.h>#include <util/fresh_symbol.h>#include <util/replace_symbol.h>#include <goto-programs/remove_skip.h>#include <analyses/local_may_alias.h>#include <linking/static_lifetime_init.h>#include "loop_utils.h"
Include dependency graph for code_contracts.cpp:Go to the source code of this file.
Classes | |
| class | code_contractst |
Functions | |
| static void | check_apply_invariants (goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop) |
| void | code_contracts (goto_modelt &goto_model) |
Detailed Description
Verify and use annotated invariants and pre/post-conditions.
Definition in file code_contracts.cpp.
Function Documentation
◆ check_apply_invariants()
|
static |
Definition at line 67 of file code_contracts.cpp.
◆ code_contracts()
| void code_contracts | ( | goto_modelt & | goto_model | ) |
Definition at line 412 of file code_contracts.cpp.
