Changeset 3040


Ignore:
Timestamp:
Mar 29, 2013, 5:51:40 PM (4 years ago)
Author:
tranquil
Message:

fixed LINToASM

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r3039 r3040  
    8888
    8989definition start_funct_translation :
    90   ∀globals.(ident × (joint_function LIN globals)) →
     90  ∀globals,functions.(ident × (joint_function LIN globals functions)) →
    9191    state_monad ASM_universe unit ≝
    92   λg,id_f,u.
     92  λg,functs,id_f,u.
    9393    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
    9494      (fresh_cost_label … u), it〉.
     
    244244        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    245245        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    246         | ADDRESS id proof _ _ ⇒
     246        | ADDRESS id proof off _ _ ⇒
    247247          ! Id ← Identifier_of_ident … id ;
    248           return (Mov (inl ?? DPTR) Id (bv_zero ?))
     248          return (Mov (inl ?? DPTR) Id off)
    249249        | SET_CARRY ⇒
    250250          return Instruction (SETB ? CARRY)
     
    339339
    340340definition translate_fun_def ≝
    341   λglobals.
    342   λid_def : ident × (joint_function LIN globals).
     341  λglobals,functions.
     342  λid_def : ident × (joint_function LIN globals functions).
    343343  !_ start_funct_translation … id_def ;
    344344  (* ^ modify current function id ^ *)
Note: See TracChangeset for help on using the changeset viewer.