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/CexecSound.ma

    r2176 r2353  
    337337        @step_skip_call //;
    338338    | #s' #k' whd; //
    339     | #ex #s' #k' @step_skip_or_continue_while % //;
     339    | #ex #s' #cl #k' @step_skip_or_continue_while % //;
    340340    | #ex #s' #k'
    341341        @res_bindIO2_OK #v #tr #Hv
     
    385385    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    386386    ]
    387   | #ex #s'
     387  | #ex #s' #cl
    388388    @res_bindIO2_OK #v #tr #Hv
    389389    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     
    407407  | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
    408408  | whd in ⊢ (?????%); cases k; //;
    409     [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
     409    [ #ex #s' #cl #k' whd; @step_skip_or_continue_while %2 ; //;
    410410    | #ex #s' #k' whd;
    411411      @res_bindIO2_OK #v #tr #Hv
Note: See TracChangeset for help on using the changeset viewer.