Changeset 1877 for src/RTLabs


Ignore:
Timestamp:
Apr 4, 2012, 6:48:27 PM (8 years ago)
Author:
campbell
Message:

Update RTLabs structured traces for typed binops and new memory model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1812 r1877  
    5555| whd in H:(??%?);
    5656  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
    57   normalize try #a try #b try #c try #d try #e try #g try #h destruct
     57  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    5858] qed.
    5959
     
    511511  [ @refl
    512512  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
    513     try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
     513    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
    514514    [ %1 %{A} %{B} %{C} @refl
    515515    | %2 %{A} %{B} @refl
     
    565565* [ #f #fs #m whd in ⊢ (??%? → ?);
    566566    cases (lookup_present … (next f) (next_ok f)) normalize
    567     try #A try #B try #C try #D try #E try #F try #G destruct
     567    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
    568568  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
    569569  | normalize #H411 #H412 #H413 #H414 #H415 destruct
     
    582582cases fd
    583583[ #fn whd in ⊢ (??%? → % → ?);
    584   @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
     584  @bind_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
    585585  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    586586  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
     
    682682[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
    683683  cases (lookup_present ??? (next f) (next_ok f)) in E;
    684   normalize #a try #b try #c try #d try #e try #f try #g destruct
     684  normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
    685685| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
    686686| #res #dst *
     
    11781178| St_const _ _ l ⇒ [l]
    11791179| St_op1 _ _ _ _ _ l ⇒ [l]
    1180 | St_op2 _ _ _ _ l ⇒ [l]
     1180| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
    11811181| St_load _ _ _ l ⇒ [l]
    11821182| St_store _ _ _ l ⇒ [l]
     
    12221222| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    12231223| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1224 | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1224| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    12251225| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    12261226| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     
    13141314| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    13151315| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    1316 | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1316| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    13171317| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    13181318| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
Note: See TracChangeset for help on using the changeset viewer.