Changeset 3037 for src/RTL


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

Location:
src/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r2975 r3037  
    9393
    9494(* parameters for main need to be passed to the premain *)
    95 definition RTL_premain : ∀p : rtl_program.joint_closed_internal_function RTL (prog_var_names ?? p) ≝
     95definition RTL_premain : ∀p : rtl_program.
     96  joint_closed_internal_function RTL (prog_names … p) ≝
    9697λp.
    9798let l1 : label ≝ an_identifier … one in
     
    104105    an_identifier … (p0 (p0 one)) ] in
    105106let res ≝
    106   mk_joint_internal_function RTL (prog_var_names … p)
     107  mk_joint_internal_function RTL (prog_names … p)
    107108  (mk_universe … (p0 (p0 one)))
    108109  (mk_universe … (p1 (p0 one)))
  • src/RTL/RTLToERTL.ma

    r2876 r3037  
    226226    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
    227227    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
    228     | ADDRESS x prf r1 r2 ⇒
    229       [ADDRESS ERTL ? x prf r1 r2]
     228    | ADDRESS x prf off r1 r2 ⇒
     229      [ADDRESS ERTL ? x prf off r1 r2]
    230230    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    231231      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
Note: See TracChangeset for help on using the changeset viewer.