CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
is_fresh_baset Class Referenceabstract

#include <memory_predicates.h>

+ Inheritance diagram for is_fresh_baset:
+ Collaboration diagram for is_fresh_baset:

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

code_contractst & parent
 
messaget log
 
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 19 of file memory_predicates.h.

Constructor & Destructor Documentation

◆ is_fresh_baset()

is_fresh_baset::is_fresh_baset ( code_contractst &  _parent,
messaget  _log,
const irep_idt  _fun_id 
)
inline

Definition at line 22 of file memory_predicates.h.

Member Function Documentation

◆ add_declarations()

void is_fresh_baset::add_declarations ( const std::string &  decl_string)
protected

Definition at line 164 of file memory_predicates.cpp.

◆ add_memory_map_dead()

void is_fresh_baset::add_memory_map_dead ( goto_programt &  program)

Definition at line 156 of file memory_predicates.cpp.

◆ add_memory_map_decl()

void is_fresh_baset::add_memory_map_decl ( goto_programt &  program)

Definition at line 143 of file memory_predicates.cpp.

◆ create_declarations()

virtual void is_fresh_baset::create_declarations ( )
pure virtual

Implemented in is_fresh_replacet, and is_fresh_enforcet.

◆ create_ensures_fn_call()

virtual void is_fresh_baset::create_ensures_fn_call ( goto_programt::targett &  target)
protectedpure virtual

Implemented in is_fresh_replacet, and is_fresh_enforcet.

◆ create_requires_fn_call()

virtual void is_fresh_baset::create_requires_fn_call ( goto_programt::targett &  target)
protectedpure virtual

Implemented in is_fresh_replacet, and is_fresh_enforcet.

◆ get_memmap_type()

array_typet is_fresh_baset::get_memmap_type ( )
protected

Definition at line 138 of file memory_predicates.cpp.

◆ update_ensures()

void is_fresh_baset::update_ensures ( goto_programt &  ensures)

Definition at line 122 of file memory_predicates.cpp.

◆ update_fn_call()

void is_fresh_baset::update_fn_call ( goto_programt::targett &  target,
const std::string &  name,
bool  add_address_of 
)
protected

Definition at line 225 of file memory_predicates.cpp.

◆ update_requires()

void is_fresh_baset::update_requires ( goto_programt &  requires)

Definition at line 112 of file memory_predicates.cpp.

Member Data Documentation

◆ ensures_fn_name

std::string is_fresh_baset::ensures_fn_name
protected

Definition at line 55 of file memory_predicates.h.

◆ fun_id

irep_idt is_fresh_baset::fun_id
protected

Definition at line 50 of file memory_predicates.h.

◆ log

messaget is_fresh_baset::log
protected

Definition at line 49 of file memory_predicates.h.

◆ memmap_name

std::string is_fresh_baset::memmap_name
protected

Definition at line 53 of file memory_predicates.h.

◆ memmap_symbol

symbolt is_fresh_baset::memmap_symbol
protected

Definition at line 56 of file memory_predicates.h.

◆ parent

code_contractst& is_fresh_baset::parent
protected

Definition at line 48 of file memory_predicates.h.

◆ requires_fn_name

std::string is_fresh_baset::requires_fn_name
protected

Definition at line 54 of file memory_predicates.h.

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