 Timestamp:
 Mar 27, 2013, 11:42:03 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/sum.test.ma
r2645 r2972 30 30 let 〈p0,init〉 ≝ clight_label myprog in 31 31 bind ? (snapshot state) (clight_to_cminor (simplify_program p0)) 32 (λp1. let p2 ≝ cminor_to_rtlabs initp1 in32 (λp1. let p2 ≝ cminor_to_rtlabs p1 in 33 33 exec_up_to RTLabs_fullexec p2 1000 [ ])). 34 34 normalize … … 60 60 let 〈p0,init〉 ≝ clight_label myprog in 61 61 ! p1 ← clight_to_cminor (simplify_program p0); 62 let p2 ≝ cminor_to_rtlabs initp1 in62 let p2 ≝ cminor_to_rtlabs p1 in 63 63 return (check_cost_program p2)) = OK bool true. 64 64 normalize
Note: See TracChangeset
for help on using the changeset viewer.