cprover
code_contracts.cpp File Reference

Verify and use annotated invariants and pre/post-conditions. More...

#include <algorithm>
#include <unordered_set>
#include <analyses/local_may_alias.h>
#include <goto-programs/remove_skip.h>
#include <linking/static_lifetime_init.h>
#include <util/c_types.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/message.h>
#include <util/pointer_predicates.h>
#include <util/replace_symbol.h>
#include "code_contracts.h"
#include "loop_utils.h"
+ Include dependency graph for code_contracts.cpp:

Go to the source code of this file.

Classes

class  return_value_visitort
 Predicate to be used with the exprt::visit() function. More...
 

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)
 
static exprt create_alias_expression (const exprt &assigns, const exprt &lhs, std::vector< exprt > &aliasable_references)
 

Detailed Description

Verify and use annotated invariants and pre/post-conditions.

Definition in file code_contracts.cpp.

Function Documentation

◆ check_apply_invariants()

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 
)
static

Definition at line 62 of file code_contracts.cpp.

◆ create_alias_expression()

static exprt create_alias_expression ( const exprt assigns,
const exprt lhs,
std::vector< exprt > &  aliasable_references 
)
static

Definition at line 336 of file code_contracts.cpp.