cprover
code_contracts.cpp File Reference

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

+ 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

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)
 

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 77 of file code_contracts.cpp.

◆ get_size()

exprt get_size ( const typet type,
const namespacet ns,
messaget log 
)

Definition at line 68 of file code_contracts.cpp.