rewrite_rw_ok.h File Reference

Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state. More...

This graph shows which files directly or indirectly include this file:

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. More...

Detailed Description

Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.

Definition in file rewrite_rw_ok.h.

Function Documentation

rewrite_rw_ok()

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.