Changeset 1238 for src/Clight/test/search.c.ma
- Timestamp:
- Sep 21, 2011, 4:25:36 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/search.c.ma
r1224 r1238 192 192 include "Cminor/semantics.ma". 193 193 194 example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])). 195 (* 194 196 example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]). 197 *) 195 198 normalize 196 199 @refl … … 202 205 example e2: finishes_with (repr 3) ? ( 203 206 do p1 ← clight_to_cminor myprog; 207 bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2. 208 exec_up_to RTLabs_fullexec p2 1000 [ ])). 209 (* 210 example e2: finishes_with (repr 3) ? ( 211 do p1 ← clight_to_cminor myprog; 204 212 do p2 ← cminor_to_rtlabs p1; 205 exec_up_to RTLabs_fullexec p2 1000 [ ]). 213 exec_up_to RTLabs_fullexec p2 1000 [ ]).*) 206 214 normalize 207 215 @refl
Note: See TracChangeset
for help on using the changeset viewer.