Ignore:
Timestamp:
Aug 29, 2011, 2:34:23 PM (8 years ago)
Author:
sacerdot
Message:

Added comment about missing alignment of data in memory.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r961 r1123  
    168168    [ Internal fn ⇒
    169169        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
     170        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
     171           here *)
    170172        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    171173        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
Note: See TracChangeset for help on using the changeset viewer.