CBMC
|
#include <memory_predicates.h>
Public Member Functions | |
is_fresh_baset (goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id) | |
void | update_requires (goto_programt &requires_) |
void | update_ensures (goto_programt &ensures) |
virtual void | create_declarations ()=0 |
void | add_memory_map_decl (goto_programt &program) |
void | add_memory_map_dead (goto_programt &program) |
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 |
array_typet | get_memmap_type () |
Protected Attributes | |
goto_modelt & | goto_model |
message_handlert & | message_handler |
const irep_idt & | fun_id |
std::string | memmap_name |
std::string | requires_fn_name |
std::string | ensures_fn_name |
symbolt | memmap_symbol |
Definition at line 25 of file memory_predicates.h.
|
inline |
Definition at line 28 of file memory_predicates.h.
|
protected |
Definition at line 166 of file memory_predicates.cpp.
void is_fresh_baset::add_memory_map_dead | ( | goto_programt & | program | ) |
Definition at line 158 of file memory_predicates.cpp.
void is_fresh_baset::add_memory_map_decl | ( | goto_programt & | program | ) |
Definition at line 144 of file memory_predicates.cpp.
|
pure virtual |
Implemented in is_fresh_replacet, and is_fresh_enforcet.
|
protectedpure virtual |
Implemented in is_fresh_replacet, and is_fresh_enforcet.
|
protectedpure virtual |
Implemented in is_fresh_replacet, and is_fresh_enforcet.
|
protected |
Definition at line 139 of file memory_predicates.cpp.
void is_fresh_baset::update_ensures | ( | goto_programt & | ensures | ) |
Definition at line 123 of file memory_predicates.cpp.
|
protected |
Definition at line 218 of file memory_predicates.cpp.
void is_fresh_baset::update_requires | ( | goto_programt & | requires_ | ) |
Definition at line 113 of file memory_predicates.cpp.
|
protected |
Definition at line 61 of file memory_predicates.h.
|
protected |
Definition at line 56 of file memory_predicates.h.
|
protected |
Definition at line 54 of file memory_predicates.h.
|
protected |
Definition at line 59 of file memory_predicates.h.
|
protected |
Definition at line 62 of file memory_predicates.h.
|
protected |
Definition at line 55 of file memory_predicates.h.
|
protected |
Definition at line 60 of file memory_predicates.h.