rewrite_rw_ok.cpp File Reference
#include "rewrite_rw_ok.h"#include <util/expr_iterator.h>#include <util/pointer_expr.h>#include <goto-programs/goto_model.h>
Include dependency graph for rewrite_rw_ok.cpp:Go to the source code of this file.
Functions | |
| static std::optional< exprt > | rewrite_rw_ok (exprt expr, const namespacet &ns) |
| static void | rewrite_rw_ok (goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
| 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. More... | |
Function Documentation
◆ rewrite_rw_ok() [1/3]
|
static |
Definition at line 16 of file rewrite_rw_ok.cpp.
◆ rewrite_rw_ok() [2/3]
|
static |
Definition at line 68 of file rewrite_rw_ok.cpp.
◆ rewrite_rw_ok() [3/3]
| 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.
