cprover
|
Verify and use annotated invariants and pre/post-conditions. More...
#include "code_contracts.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"
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) |
Verify and use annotated invariants and pre/post-conditions.
Definition in file code_contracts.cpp.
|
static |
Definition at line 66 of file code_contracts.cpp.
References goto_programt::add_instruction(), ASSERT, ASSUME, build_havoc_code(), goto_programt::instructiont::function, get_modifies(), GOTO, goto_programt::instructiont::guard, irept::is_nil(), source_locationt::set_comment(), typet::source_location(), exprt::source_location(), and goto_programt::instructiont::source_location.
Referenced by code_contractst::code_contracts().
void code_contracts | ( | goto_modelt & | goto_model | ) |
Definition at line 402 of file code_contracts.cpp.
References goto_modelt::goto_functions, and goto_modelt::symbol_table.
Referenced by goto_instrument_parse_optionst::instrument_goto_program().