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

    r1713 r2353  
    514514#ge #s cases s;
    515515[ #f #st #kk #e #m cases st;
    516   [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
    517   [ 4,6,8,9: @I ]
     516  [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
     517  [ 4,5,7,8: @I ]
    518518  whd in ⊢ (???%);
    519519  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
     
    521521  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
    522522  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
    523   | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    524523  | @err2_does_not_interact #x1 #x2 cases x1; //;
    525524  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
    526525      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
     526  | 6,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    527527  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    528528      | @I ]
Note: See TracChangeset for help on using the changeset viewer.