Changeset 2824 for src/joint/Traces.ma


Ignore:
Timestamp:
Mar 8, 2013, 5:37:57 PM (7 years ago)
Author:
tranquil
Message:
  • moved sum on lists notation to extranat
  • used sum on lists to define portion of stack occupied by globals
  • corrected probable bug in joint semantics, where initial state would not move stack pointer past globals before setting up main
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2821 r2824  
    7272  let m0 ≝ alloc_mem … p in
    7373  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
     74  let globals_size ≝ globals_stacksize … p in
     75  (* stack pointer should start at 2^16 - |globals|, right?
     76     first call to main shuold bring it to 2^16 - |globals| - |main stack|
     77     Also, on words 2^16 - |globals| = - |globals| *)
    7478  let spp : xpointer ≝
    75     «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
     79    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-globals_size))),
    7680     pi2 … spb» in
    7781(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
Note: See TracChangeset for help on using the changeset viewer.