CBMC
Public Member Functions | Protected Member Functions | List of all members
is_fresh_enforcet Class Reference

#include <memory_predicates.h>

+ Inheritance diagram for is_fresh_enforcet:
+ Collaboration diagram for is_fresh_enforcet:

Public Member Functions

 is_fresh_enforcet (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
 

Detailed Description

Definition at line 67 of file memory_predicates.h.

Constructor & Destructor Documentation

◆ is_fresh_enforcet()

is_fresh_enforcet::is_fresh_enforcet ( goto_modelt &  goto_model,
message_handlert &  message_handler,
const irep_idt &  _fun_id 
)

Definition at line 242 of file memory_predicates.cpp.

Member Function Documentation

◆ create_declarations()

void is_fresh_enforcet::create_declarations ( )
virtual

Implements is_fresh_baset.

Definition at line 268 of file memory_predicates.cpp.

◆ create_ensures_fn_call()

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

Implements is_fresh_baset.

Definition at line 316 of file memory_predicates.cpp.

◆ create_requires_fn_call()

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

Implements is_fresh_baset.

Definition at line 311 of file memory_predicates.cpp.

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