CBMC
rewrite_rw_ok.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
12 
13 #ifndef CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
14 #define CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
15 
16 class goto_modelt;
17 
25 void rewrite_rw_ok(goto_modelt &);
26 
27 #endif // CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
goto_modelt
Definition: goto_model.h:27
rewrite_rw_ok
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 proph...
Definition: rewrite_rw_ok.cpp:77