Changeset 1123 for src/RTLabs/semantics.ma

Timestamp:

Aug 29, 2011, 2:34:23 PM (10 years ago)

Author:

sacerdot

Message:

Added comment about missing alignment of data in memory.

File:

• src/RTLabs/semantics.ma (modified) (1 diff)

src/RTLabs/semantics.ma

@@ -168 +168 @@
     [ Internal fn ⇒
         ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
+        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
+           here *)
         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉