Changeset 1874 for src/RTLabs


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

First cut at using back-end memory model throughout.
Note the correction to BEValues.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1872 r1874  
    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 ⇒
     
    313313| * #fn #args #retdst #stk #m #tr #s'
    314314  whd in ⊢ (??%? → ?);
    315   [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     315  [ @bind_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
    316316    #E destruct %3
    317317  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
Note: See TracChangeset for help on using the changeset viewer.