cprover
|
#include "rewrite_rw_ok.h"
#include <util/expr_iterator.h>
#include <util/pointer_expr.h>
#include <goto-programs/goto_model.h>
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. |
|
static |
Definition at line 16 of file rewrite_rw_ok.cpp.
|
static |
Definition at line 68 of file rewrite_rw_ok.cpp.
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.