cprover
|
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state. More...
Go to the source code of this file.
Functions | |
void | rewrite_rw_ok (goto_modelt &) |
Replace all occurrences of r_ok_exprt, w_ok_exprt, rw_ok_exprt, pointer_in_range_exprt by their prophecy variants prophecy_r_or_w_ok_exprt and prophecy_pointer_in_range_exprt, respectively. |
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
Definition in file rewrite_rw_ok.h.
void rewrite_rw_ok | ( | goto_modelt & | goto_model | ) |
Replace all occurrences of r_ok_exprt, w_ok_exprt, rw_ok_exprt, pointer_in_range_exprt by their prophecy variants prophecy_r_or_w_ok_exprt and prophecy_pointer_in_range_exprt, respectively.
Each analysis may choose to natively support r_ok_exprt etc. (like cprover_parse_optionst does) or may instead require the expression to be lowered to other primitives (like goto_symext).
Definition at line 77 of file rewrite_rw_ok.cpp.