Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (7 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1986 r1988  
    167167                return (Some ? v)
    168168            ];
    169       return 〈E0, Returnstate v (retdst f) fs (free ? m (sp f))〉
     169      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    170170  ] (f_closed (func f) (next f) s ?)
    171171| Callstate fd params dst fs m ⇒
     
    175175        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
    176176           here *)
    177         let 〈m', sp〉 ≝ alloc ? m 0 (f_stacksize fn) Any in
     177        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    178178        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    179179    | External fn ⇒
     
    295295| * #fn #args #retdst #stk #m #tr #s'
    296296  whd in ⊢ (??%? → ?);
    297   [ @bind_res_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
     297  [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
    298298    #E destruct %3
    299299  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
Note: See TracChangeset for help on using the changeset viewer.