cprover
|
Verify and use annotated invariants and pre/post-conditions. More...
#include "code_contracts.h"
#include <algorithm>
#include <analyses/local_may_alias.h>
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/remove_skip.h>
#include <linking/static_lifetime_init.h>
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/expr_util.h>
#include <util/format_type.h>
#include <util/fresh_symbol.h>
#include <util/mathematical_expr.h>
#include <util/mathematical_types.h>
#include <util/message.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/replace_symbol.h>
#include "loop_utils.h"
Go to the source code of this file.
Classes | |
class | return_value_visitort |
Predicate to be used with the exprt::visit() function. More... | |
Functions | |
exprt | get_size (const typet &type, const namespacet &ns, messaget &log) |
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) |
Verify and use annotated invariants and pre/post-conditions.
Definition in file code_contracts.cpp.
|
static |
Definition at line 77 of file code_contracts.cpp.
exprt get_size | ( | const typet & | type, |
const namespacet & | ns, | ||
messaget & | log | ||
) |
Definition at line 68 of file code_contracts.cpp.