Changeset 2353 for src/Clight/test/gotoif.test.ma
 Timestamp:
 Sep 26, 2012, 6:14:38 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/gotoif.test.ma
r2253 r2353 8 8 include "Clight/label.ma". 9 9 10 definition myprog' ≝ clight_label myprog.10 definition myprog' ≝ \fst (clight_label myprog). 11 11 12 12 example el: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog' 1000 [ ]). … … 37 37 example e2: finishes_with (repr I32 0) ? ( 38 38 bind ? (snapshot state) (clight_to_cminor (simplify_program myprog')) 39 (λp1. let p2 ≝ cminor_to_rtlabs p1 in39 (λp1. let p2 ≝ cminor_to_rtlabs (\snd (clight_label myprog)) p1 in 40 40 exec_up_to RTLabs_fullexec p2 1000 [ ])). 41 41 normalize 42 42 % 43 43 qed. 44 45 include "RTLabs/CostCheck.ma". 46 47 axiom MISSING:String. 48 axiom EXTERNAL:String. 49 50 definition readable_body ≝ 51 λfn. insert_sort ? 52 (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z])) 53 (elements ?? (f_graph fn)). 54 (* 55 example c2: result ? ( 56 ! p1 ← clight_to_cminor (simplify_program (clight_label myprog)); 57 let p2 ≝ cminor_to_rtlabs p1 in 58 match prog_funct … p2 with 59 [ nil ⇒ Error ? (msg MISSING) 60  cons h _ ⇒ 61 match \snd h with 62 [ External _ ⇒ Error ? (msg EXTERNAL) 63  Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉 64 ] 65 ]). 66 normalize 67 *) 68 example c2: ( 69 let 〈p0,init〉 ≝ clight_label myprog in 70 ! p1 ← clight_to_cminor (simplify_program p0); 71 let p2 ≝ cminor_to_rtlabs init p1 in 72 return (check_cost_program p2)) = OK … true. 73 normalize 74 % 75 qed.
Note: See TracChangeset
for help on using the changeset viewer.