cprover
Loading...
Searching...
No Matches
is_fresh_replacet Class Reference

#include <memory_predicates.h>

Inheritance diagram for is_fresh_replacet:
Collaboration diagram for is_fresh_replacet:

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_modeltgoto_model
message_handlertmessage_handler
const irep_idtfun_id
std::string memmap_name
std::string requires_fn_name
std::string ensures_fn_name
symbolt memmap_symbol

Detailed Description

Definition at line 82 of file memory_predicates.h.

Constructor & Destructor Documentation

◆ is_fresh_replacet()

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.

Member Function Documentation

◆ create_declarations()

void is_fresh_replacet::create_declarations ( )
virtual

Implements is_fresh_baset.

Definition at line 347 of file memory_predicates.cpp.

◆ create_ensures_fn_call()

void is_fresh_replacet::create_ensures_fn_call ( goto_programt::targett & target)
protectedvirtual

Implements is_fresh_baset.

Definition at line 394 of file memory_predicates.cpp.

◆ create_requires_fn_call()

void is_fresh_replacet::create_requires_fn_call ( goto_programt::targett & target)
protectedvirtual

Implements is_fresh_baset.

Definition at line 389 of file memory_predicates.cpp.


The documentation for this class was generated from the following files: