Changeset 816 for src/Clight/test
- Timestamp:
- May 19, 2011, 3:06:42 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/search.ma
r748 r816 193 193 @refl 194 194 qed. 195 196 include "Clight/toCminor.ma". 197 include "Cminor/semantics.ma". 198 199 example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]). 200 normalize 201 @refl 202 qed. 203 204 include "Cminor/toRTLabs.ma". 205 include "RTLabs/semantics.ma". 206 207 example e2: finishes_with (repr 3) ? ( 208 do p1 ← clight_to_cminor myprog; 209 do p2 ← cminor_to_rtlabs p1; 210 exec_up_to RTLabs_fullexec p2 1000 [ ]). 211 normalize 212 @refl 213 qed.
Note: See TracChangeset
for help on using the changeset viewer.