Changeset 1198 for src/Clight/test/sum.c.ma
 Timestamp:
 Sep 8, 2011, 4:04:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.