Changeset 1332 for src/Clight/test/sum.test.ma
 Timestamp:
 Oct 10, 2011, 12:41:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/sum.test.ma
r1226 r1332 16 16 include "Cminor/semantics.ma". 17 17 18 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]). 18 example e1: finishes_with (repr I32 74) ? 19 (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) 20 (λp. exec_up_to Cminor_fullexec p 1000 [ ])). 19 21 normalize 20 22 @refl … … 25 27 26 28 example e2: finishes_with (repr I32 74) ? ( 27 do p1 ← clight_to_cminor (simplify_program myprog); 28 do p2 ← cminor_to_rtlabs p1; 29 exec_up_to RTLabs_fullexec p2 1000 [ ]).29 bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) 30 (λp1. bind ? (snapshot state) (cminor_to_rtlabs p1) 31 (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))). 30 32 normalize 31 33 @refl
Note: See TracChangeset
for help on using the changeset viewer.