cprover
|
#include <memory_predicates.h>
Public Member Functions | |
is_fresh_baset (code_contractst &_parent, messaget _log, const irep_idt _fun_id) | |
void | update_requires (goto_programt &requires) |
void | update_ensures (goto_programt &ensures) |
virtual void | create_declarations ()=0 |
Protected Member Functions | |
void | add_declarations (const std::string &decl_string) |
void | update_fn_call (goto_programt::targett &target, const std::string &name, bool add_address_of) |
virtual void | create_requires_fn_call (goto_programt::targett &target)=0 |
virtual void | create_ensures_fn_call (goto_programt::targett &target)=0 |
Protected Attributes | |
code_contractst & | parent |
messaget | log |
irep_idt | fun_id |
std::string | memmap_name |
std::string | requires_fn_name |
std::string | ensures_fn_name |
Definition at line 19 of file memory_predicates.h.
|
inline |
Definition at line 22 of file memory_predicates.h.
|
protected |
Definition at line 146 of file memory_predicates.cpp.
Implemented in is_fresh_enforcet, and is_fresh_replacet.
|
protectedpure virtual |
Implemented in is_fresh_enforcet, and is_fresh_replacet.
|
protectedpure virtual |
Implemented in is_fresh_enforcet, and is_fresh_replacet.
void is_fresh_baset::update_ensures | ( | goto_programt & | ensures | ) |
Definition at line 130 of file memory_predicates.cpp.
|
protected |
Definition at line 207 of file memory_predicates.cpp.
void is_fresh_baset::update_requires | ( | goto_programt & | requires | ) |
Definition at line 120 of file memory_predicates.cpp.
|
protected |
Definition at line 52 of file memory_predicates.h.
|
protected |
Definition at line 47 of file memory_predicates.h.
|
protected |
Definition at line 46 of file memory_predicates.h.
|
protected |
Definition at line 50 of file memory_predicates.h.
|
protected |
Definition at line 45 of file memory_predicates.h.
|
protected |
Definition at line 51 of file memory_predicates.h.