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:

[フレーム]

[legend]

+ Collaboration diagram for is_fresh_baset:

[フレーム]

[legend]

Public Member Functions

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)

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

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 25 of file memory_predicates.h.

Constructor & Destructor Documentation

◆ is_fresh_baset()

is_fresh_baset::is_fresh_baset ( goto_modelt & goto_model,

message_handlert & message_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_programt & program )

Definition at line 158 of file memory_predicates.cpp.

◆ add_memory_map_decl()

void is_fresh_baset::add_memory_map_decl ( goto_programt & program )

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::targett & target )

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::targett & target )

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_programt & ensures )

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

◆ update_requires()

void is_fresh_baset::update_requires ( goto_programt & requires_ )

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:

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/memory_predicates.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/memory_predicates.cpp