Changeset 3037 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (7 years ago)
Author:
tranquil
Message:
  • ADDRESS joint instruction now has also an offset
  • corrected call to pointer (needed to clear the accumulator)
  • now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2952 r3037  
    125125  on _s : ertl_seq to joint_seq ERTL ?.
    126126
    127 definition ERTL_premain : ∀p : ertl_program.joint_closed_internal_function ERTL (prog_var_names ?? p) ≝
     127definition ERTL_premain : ∀p : ertl_program.
     128  joint_closed_internal_function ERTL (prog_names … p) ≝
    128129λp.
    129130let l1 : label ≝ an_identifier … one in
     
    131132let l3 : label ≝ an_identifier … (p1 one) in
    132133let res ≝
    133   mk_joint_internal_function ERTL (prog_var_names … p)
     134  mk_joint_internal_function ERTL (prog_names … p)
    134135  (mk_universe … (p0 (p0 one)))
    135136  (mk_universe … one)
Note: See TracChangeset for help on using the changeset viewer.