Changeset 3014 for src/joint


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (7 years ago)
Author:
tranquil
Message:

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2991 r3014  
    3333     first call to main shuold bring it to 2^16 - |globals| - |main stack|
    3434     Also, on words 2^16 - |globals| = - |globals| *)
     35  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    3536  let spp : xpointer ≝
    36     «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-globals_size))),
     37    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size)))),
    3738     pi2 … spb» in
    3839(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
Note: See TracChangeset for help on using the changeset viewer.