CBMC
|
Rewrites calls to is_fresh predicates into calls to the library implementation. More...
#include <dfcc_is_fresh.h>
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_libraryt & | library |
message_handlert & | message_handler |
messaget | log |
Rewrites calls to is_fresh predicates into calls to the library implementation.
Definition at line 29 of file dfcc_is_fresh.h.
dfcc_is_fresht::dfcc_is_fresht | ( | dfcc_libraryt & | library, |
message_handlert & | message_handler | ||
) |
library | The contracts instrumentation library |
message_handler | Used for messages |
Definition at line 19 of file dfcc_is_fresh.cpp.
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.
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.
|
protected |
Definition at line 52 of file dfcc_is_fresh.h.
|
protected |
Definition at line 54 of file dfcc_is_fresh.h.
|
protected |
Definition at line 53 of file dfcc_is_fresh.h.