Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/goto-if.test.ma

    r2253 r2353  
    88include "Clight/label.ma".
    99
    10 definition myprog' ≝ clight_label myprog.
     10definition myprog' ≝ \fst (clight_label myprog).
    1111
    1212example el: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog' 1000 [ ]).
     
    3737example e2: finishes_with (repr I32 0) ? (
    3838bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
    39 (λp1. let p2 ≝ cminor_to_rtlabs p1 in
     39(λp1. let p2 ≝ cminor_to_rtlabs (\snd (clight_label myprog)) p1 in
    4040  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    4141normalize
    4242%
    4343qed.
     44
     45include "RTLabs/CostCheck.ma".
     46
     47axiom MISSING:String.
     48axiom EXTERNAL:String.
     49
     50definition 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(*
     55example 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  ]).
     66normalize
     67*)
     68example 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.
     73normalize
     74%
     75qed.
Note: See TracChangeset for help on using the changeset viewer.