CBMC
|
#include <memory_predicates.h>
Public Member Functions | |
is_fresh_replacet (goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id) | |
virtual void | create_declarations () |
Public Member Functions inherited from is_fresh_baset | |
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) |
void | add_memory_map_decl (goto_programt &program) |
void | add_memory_map_dead (goto_programt &program) |
Protected Member Functions | |
virtual void | create_requires_fn_call (goto_programt::targett &target) |
virtual void | create_ensures_fn_call (goto_programt::targett &target) |
Protected Member Functions inherited from is_fresh_baset | |
void | add_declarations (const std::string &decl_string) |
void | update_fn_call (goto_programt::targett &target, const std::string &name, bool add_address_of) |
array_typet | get_memmap_type () |
Additional Inherited Members | |
Protected Attributes inherited from is_fresh_baset | |
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 82 of file memory_predicates.h.
is_fresh_replacet::is_fresh_replacet | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
const irep_idt & | _fun_id | ||
) |
Definition at line 321 of file memory_predicates.cpp.
|
virtual |
Implements is_fresh_baset.
Definition at line 347 of file memory_predicates.cpp.
|
protectedvirtual |
Implements is_fresh_baset.
Definition at line 394 of file memory_predicates.cpp.
|
protectedvirtual |
Implements is_fresh_baset.
Definition at line 389 of file memory_predicates.cpp.