Changeset 1311 for Deliverables/D3.3/id-lookup-branch/Cminor/test
- Timestamp:
- Oct 6, 2011, 6:45:54 PM (9 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 2 edited
- 1 copied
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1198,1206-1233,1236-1260,1262-1264,1266,1268-1271,1274-1276,1278-1290,1292
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma
r1197 r1311 281 281 282 282 definition myprog : Cminor_program := 283 mk_program ?? [ 283 mk_program ?? [] [ 284 284 (pair ?? id__div32u f__div32u); 285 285 (pair ?? id__div32s f__div32s); … … 287 287 (pair ?? id_main f_main) 288 288 ] id_main 289 []290 289 . 291 292 example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).293 normalize (* you can examine the result here *)294 @refl qed.295 296 297 include "Cminor/toRTLabs.ma".298 include "RTLabs/semantics.ma".299 300 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).301 normalize (* you can examine the result here *)302 @refl303 qed.304 305
Note: See TracChangeset
for help on using the changeset viewer.