CBMC
|
Rewrites calls to pointer_equals predicates into calls to the library implementation. More...
#include <dfcc_pointer_equals.h>
Public Member Functions | |
dfcc_pointer_equalst (dfcc_libraryt &library, message_handlert &message_handler) | |
void | rewrite_calls (goto_programt &program, dfcc_cfg_infot cfg_info) |
Rewrites calls to pointer_equals predicates into calls to the library implementation in the given program, passing the given write_set expression as parameter to the library function. | |
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 pointer_equals 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. | |
Protected Attributes | |
dfcc_libraryt & | library |
message_handlert & | message_handler |
messaget | log |
Rewrites calls to pointer_equals predicates into calls to the library implementation.
Definition at line 35 of file dfcc_pointer_equals.h.
dfcc_pointer_equalst::dfcc_pointer_equalst | ( | dfcc_libraryt & | library, |
message_handlert & | message_handler | ||
) |
library | The contracts instrumentation library |
message_handler | Used for messages |
Definition at line 26 of file dfcc_pointer_equals.cpp.
void dfcc_pointer_equalst::rewrite_calls | ( | goto_programt & | program, |
dfcc_cfg_infot | cfg_info | ||
) |
Rewrites calls to pointer_equals 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 33 of file dfcc_pointer_equals.cpp.
void dfcc_pointer_equalst::rewrite_calls | ( | goto_programt & | program, |
goto_programt::targett | first_instruction, | ||
const goto_programt::targett & | last_instruction, | ||
dfcc_cfg_infot | cfg_info | ||
) |
Rewrites calls to pointer_equals 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 44 of file dfcc_pointer_equals.cpp.
|
protected |
Definition at line 60 of file dfcc_pointer_equals.h.
|
protected |
Definition at line 62 of file dfcc_pointer_equals.h.
|
protected |
Definition at line 61 of file dfcc_pointer_equals.h.