CBMC
|
Rewrites calls to pointer_in_range predicates into calls to the library implementation. More...
#include <dfcc_pointer_in_range.h>
Public Member Functions | |
dfcc_pointer_in_ranget (dfcc_libraryt &library, message_handlert &message_handler) | |
void | rewrite_calls (goto_programt &program, dfcc_cfg_infot cfg_info) |
Rewrites calls to pointer_in_range 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 pointer_in_range 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 pointer_in_range predicates into calls to the library implementation.
Definition at line 29 of file dfcc_pointer_in_range.h.
dfcc_pointer_in_ranget::dfcc_pointer_in_ranget | ( | dfcc_libraryt & | library, |
message_handlert & | message_handler | ||
) |
library | The contracts instrumentation library |
message_handler | Used for messages |
Definition at line 21 of file dfcc_pointer_in_range.cpp.
void dfcc_pointer_in_ranget::rewrite_calls | ( | goto_programt & | program, |
dfcc_cfg_infot | cfg_info | ||
) |
Rewrites calls to pointer_in_range 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 28 of file dfcc_pointer_in_range.cpp.
void dfcc_pointer_in_ranget::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_in_range 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 39 of file dfcc_pointer_in_range.cpp.
|
protected |
Definition at line 54 of file dfcc_pointer_in_range.h.
|
protected |
Definition at line 56 of file dfcc_pointer_in_range.h.
|
protected |
Definition at line 55 of file dfcc_pointer_in_range.h.