CBMC
dfcc_is_fresht Class Reference

Rewrites calls to is_fresh predicates into calls to the library implementation. More...

#include <dfcc_is_fresh.h>

+ Collaboration diagram for dfcc_is_fresht:

Public Member Functions

 dfcc_is_fresht (dfcc_libraryt &library, message_handlert &message_handler)
 
void rewrite_calls (goto_programt &program, dfcc_cfg_infot &cfg_info)
 Rewrites calls to is_fresh predicates into calls to the library implementation in the given program, passing the given write_set expression as parameter to the library function. More...
 
void rewrite_calls (goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info)
 Rewrites calls to is_fresh predicates into calls to the library implementation in the given program between first_instruction (included) and last_instruction (excluded), passing the given write_set expression as parameter to the library function. More...
 

Protected Attributes

dfcc_librarytlibrary
 
message_handlertmessage_handler
 
messaget log
 

Detailed Description

Rewrites calls to is_fresh predicates into calls to the library implementation.

Definition at line 29 of file dfcc_is_fresh.h.

Constructor & Destructor Documentation

◆ dfcc_is_fresht()

dfcc_is_fresht::dfcc_is_fresht ( dfcc_libraryt library,
message_handlert message_handler 
)
Parameters
libraryThe contracts instrumentation library
message_handlerUsed for messages

Definition at line 19 of file dfcc_is_fresh.cpp.

Member Function Documentation

◆ rewrite_calls() [1/2]

void dfcc_is_fresht::rewrite_calls ( goto_programt program,
dfcc_cfg_infot cfg_info 
)

Rewrites calls to is_fresh predicates into calls to the library implementation in the given program, passing the given write_set expression as parameter to the library function.

Definition at line 26 of file dfcc_is_fresh.cpp.

◆ rewrite_calls() [2/2]

void dfcc_is_fresht::rewrite_calls ( goto_programt program,
goto_programt::targett  first_instruction,
const goto_programt::targett last_instruction,
dfcc_cfg_infot cfg_info 
)

Rewrites calls to is_fresh predicates into calls to the library implementation in the given program between first_instruction (included) and last_instruction (excluded), passing the given write_set expression as parameter to the library function.

Definition at line 37 of file dfcc_is_fresh.cpp.

Member Data Documentation

◆ library

dfcc_libraryt& dfcc_is_fresht::library
protected

Definition at line 52 of file dfcc_is_fresh.h.

◆ log

messaget dfcc_is_fresht::log
protected

Definition at line 54 of file dfcc_is_fresh.h.

◆ message_handler

message_handlert& dfcc_is_fresht::message_handler
protected

Definition at line 53 of file dfcc_is_fresh.h.


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