Changeset 3037 for src/RTLabs


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/RTLabs/RTLabsToRTL.ma

    r3004 r3037  
    327327  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    328328    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    329     ADDRESS RTL globals id ? r1 r2 ::
    330     if eqb offset 0 then [ ] else
    331     translate_op … Add
    332       [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ]
    333       (refl …) (refl …)
     329    let off ≝ bitvector_of_nat 16 offset in
     330    [ ADDRESS RTL globals id ? off r1 r2 ]
    334331  | Oaddrstack offset ⇒ λcst_prf,prf.
    335332    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     
    11091106 λinit_cost, p.
    11101107  mk_joint_program …
    1111     (transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)))
    1112     init_cost.
     1108    (prog_funct_names \ldots p)
     1109    (transform_program … p (λvarnames. transf_fundef … (translate_internal ?)))
     1110    init_cost
     1111    ?.
     1112@hide_prf @transform_prog_funct_names qed.
Note: See TracChangeset for help on using the changeset viewer.