Changeset 1198 for src/Clight
 Timestamp:
 Sep 8, 2011, 4:04:07 PM (9 years ago)
 Location:
 src/Clight
 Files:

 3 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/TypeComparison.ma
r891 r1198 91 91 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝ 92 92 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p  inr _ ⇒ Error ? (msg TypeMismatch)]. 93 94 definition type_eq : type → type → bool ≝ 95 λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true  inr _ ⇒ false ]. 96 
src/Clight/test/sum.c.ma
r1139 r1198 60 60 qed. 61 61 62 include "Clight/SimplifyCasts.ma". 63 64 example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]). 65 normalize (* you can examine the result here *) 66 @refl 67 qed. 68 62 69 include "Clight/toCminor.ma". 63 70 include "Cminor/semantics.ma". 64 71 65 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).72 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]). 66 73 normalize 67 74 @refl … … 72 79 73 80 example e2: finishes_with (repr I32 74) ? ( 74 do p1 ← clight_to_cminor myprog;81 do p1 ← clight_to_cminor (simplify_program myprog); 75 82 do p2 ← cminor_to_rtlabs p1; 76 83 exec_up_to RTLabs_fullexec p2 1000 [ ]).
Note: See TracChangeset
for help on using the changeset viewer.