Changeset 2176 for src/RTLabs


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2103 r2176  
    5050      isize' ÷ (nat_of_bitvector ? int_size)
    5151  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
    52   | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
     52  | ASTptr ⇒ nat_of_bitvector ? ptr_size
    5353  ].
    5454  cases not_implemented;
  • src/RTLabs/semantics.ma

    r2044 r2176  
    172172        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
    173173           here *)
    174         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
     174        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) XData in
    175175        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    176176    | External fn ⇒
     
    281281  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    282282  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ???) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    283   | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ???) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     283  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #b * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ???) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    284284(*
    285285  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     
    287287*)
    288288  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    289   | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_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 ]
     289  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_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 % % ] | *: [ 1,3: #vl ] #E whd in E:(??%?); destruct ]
    290290  | #LP whd in ⊢ (??%? → ?); @bind_res_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
    291291  ]
     
    320320    [ %{v} @Efd
    321321    | cases v in Efd;
    322       [ 5: * #pty #b #pc #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
     322      [ 5: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
    323323           [ #E @E | #E normalize in E; destruct ]
    324324      | *: normalize #A try #B try #C destruct
     
    335335  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    336336  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
    337   | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_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 ]
     337  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_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 ] | *: [1,3: #vl] #E whd in E:(??%?); destruct ]
    338338  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct
    339339  ]
Note: See TracChangeset for help on using the changeset viewer.