Ignore:
Timestamp:
Feb 9, 2012, 1:22:32 PM (7 years ago)
Author:
campbell
Message:

Checkpoint of stack preservation work in RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1680 r1681  
    245245| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
    246246| to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
     247(*
    247248| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
     249*)
    248250| from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')
    249251| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
     
    301303  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    302304  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
    303   | #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
     305  | #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
    304306  ]
    305307| * #fn #args #retdst #stk #m #tr #s'
    306308  whd in ⊢ (??%? → ?);
    307309  [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
    308     #E destruct %4
     310    #E destruct %3
    309311  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
    310312  ]
     
    312314  whd in ⊢ (??%? → ?);
    313315  [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
    314     %6 cases f #func #locals #next #next_ok #sp #retdst %
     316    %5 cases f #func #locals #next #next_ok #sp #retdst %
    315317  | #E destruct
    316318  ]
Note: See TracChangeset for help on using the changeset viewer.