Changeset 1877 for src/RTLabs/Traces.ma

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:

• src/RTLabs/Traces.ma (modified) (8 diffs)

src/RTLabs/Traces.ma

@@ -55 +55 @@
 | whd in H:(??%?);
   cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
-  normalize try #a try #b try #c try #d try #e try #g try #h destruct
+  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
 ] qed.
 
@@ -511 +511 @@
   [ @refl
   | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
-    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
+    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
     [ %1 %{A} %{B} %{C} @refl
     | %2 %{A} %{B} @refl
@@ -565 +565 @@
 * [ #f #fs #m whd in ⊢ (??%? → ?);
     cases (lookup_present … (next f) (next_ok f)) normalize
-    try #A try #B try #C try #D try #E try #F try #G destruct
+    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
   | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
   | normalize #H411 #H412 #H413 #H414 #H415 destruct
@@ -582 +582 @@
 cases fd
 [ #fn whd in ⊢ (??%? → % → ?);
-  @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
+  @bind_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
   #m' #b whd in ⊢ (??%? → ?); #E' destruct
   * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
@@ -682 +682 @@
 [ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
   cases (lookup_present ??? (next f) (next_ok f)) in E;
-  normalize #a try #b try #c try #d try #e try #f try #g destruct
+  normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
 | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
 | #res #dst *
@@ -1178 +1178 @@
 | St_const _ _ l ⇒ [l]
 | St_op1 _ _ _ _ _ l ⇒ [l]
-| St_op2 _ _ _ _ l ⇒ [l]
+| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
 | St_load _ _ _ l ⇒ [l]
 | St_store _ _ _ l ⇒ [l]
@@ -1222 +1222 @@
 | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
 | #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} % // % //
-| #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} % // % //
+| #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} % // % //
 | #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} % // % //
 | #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} % // % //
@@ -1314 +1314 @@
 | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
 | #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
-| #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
+| #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
 | #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
 | #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl