CBMC
Loading...
Searching...
No Matches
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

 
 
 
 
 
 

Protected Member Functions

 
 
 
 
 

Protected Attributes

 
 
 
std::string  memmap_name
 
std::string  requires_fn_name
 
std::string  ensures_fn_name
 
 

Detailed Description

Definition at line 25 of file memory_predicates.h.

Constructor & Destructor Documentation

◆  is_fresh_baset()

is_fresh_baset::is_fresh_baset ( goto_modeltgoto_model,
message_handlertmessage_handler,
const irep_idt_fun_id 
)
inline

Definition at line 28 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 166 of file memory_predicates.cpp.

◆  add_memory_map_dead()

void is_fresh_baset::add_memory_map_dead ( goto_programtprogram )

Definition at line 158 of file memory_predicates.cpp.

◆  add_memory_map_decl()

void is_fresh_baset::add_memory_map_decl ( goto_programtprogram )

Definition at line 144 of file memory_predicates.cpp.

◆  create_declarations()

virtual void is_fresh_baset::create_declarations ( )
pure virtual

Implemented in is_fresh_enforcet, and is_fresh_replacet.

◆  create_ensures_fn_call()

virtual void is_fresh_baset::create_ensures_fn_call ( goto_programt::targetttarget )
protectedpure virtual

Implemented in is_fresh_enforcet, and is_fresh_replacet.

◆  create_requires_fn_call()

virtual void is_fresh_baset::create_requires_fn_call ( goto_programt::targetttarget )
protectedpure virtual

Implemented in is_fresh_enforcet, and is_fresh_replacet.

◆  get_memmap_type()

array_typet is_fresh_baset::get_memmap_type ( )
protected

Definition at line 139 of file memory_predicates.cpp.

◆  update_ensures()

void is_fresh_baset::update_ensures ( goto_programtensures )

Definition at line 123 of file memory_predicates.cpp.

◆  update_fn_call()

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

Definition at line 218 of file memory_predicates.cpp.

◆  update_requires()

void is_fresh_baset::update_requires ( goto_programtrequires_ )

Definition at line 113 of file memory_predicates.cpp.

Member Data Documentation

◆  ensures_fn_name

std::string is_fresh_baset::ensures_fn_name
protected

Definition at line 61 of file memory_predicates.h.

◆  fun_id

const irep_idt& is_fresh_baset::fun_id
protected

Definition at line 56 of file memory_predicates.h.

◆  goto_model

goto_modelt& is_fresh_baset::goto_model
protected

Definition at line 54 of file memory_predicates.h.

◆  memmap_name

std::string is_fresh_baset::memmap_name
protected

Definition at line 59 of file memory_predicates.h.

◆  memmap_symbol

symbolt is_fresh_baset::memmap_symbol
protected

Definition at line 62 of file memory_predicates.h.

◆  message_handler

message_handlert& is_fresh_baset::message_handler
protected

Definition at line 55 of file memory_predicates.h.

◆  requires_fn_name

std::string is_fresh_baset::requires_fn_name
protected

Definition at line 60 of file memory_predicates.h.


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

AltStyle によって変換されたページ (->オリジナル) /