Changeset 881 for src/Clight/test
- Timestamp:
- Jun 3, 2011, 5:35:31 PM (10 years ago)
- Location:
- src/Clight/test
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/io.ma
r797 r881 28 28 @refl 29 29 qed. 30 31 32 include "Clight/toCminor.ma". 33 include "Cminor/semantics.ma". 34 35 example e1: (do p ← clight_to_cminor myprog; 36 do r ← exec_up_to Cminor_fullexec p 1000 [EVint (repr 7) ]; 37 match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) = 38 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉. 39 normalize 40 @refl 41 qed. 42 43 include "Cminor/toRTLabs.ma". 44 include "RTLabs/semantics.ma". 45 46 example e2: (do p1 ← clight_to_cminor myprog; 47 do p2 ← cminor_to_rtlabs p1; 48 do r ← exec_up_to RTLabs_fullexec p2 1000 [EVint (repr 7) ]; 49 match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) = 50 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉. 51 normalize 52 @refl 53 qed. -
src/Clight/test/sum.ma
r758 r881 60 60 @refl 61 61 qed. 62 63 include "Clight/toCminor.ma". 64 include "Cminor/semantics.ma". 65 66 example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]). 67 normalize 68 @refl 69 qed. 70 71 include "Cminor/toRTLabs.ma". 72 include "RTLabs/semantics.ma". 73 74 example e2: finishes_with (repr 74) ? ( 75 do p1 ← clight_to_cminor myprog; 76 do p2 ← cminor_to_rtlabs p1; 77 exec_up_to RTLabs_fullexec p2 1000 [ ]). 78 normalize 79 @refl 80 qed.
Note: See TracChangeset
for help on using the changeset viewer.