Changeset 3037 for src/LIN


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (8 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/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r2952 r3037  
    2929unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN.
    3030
    31 definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝
     31definition LIN_premain : ∀p : lin_program.
     32  joint_closed_internal_function LIN (prog_names … p) ≝
    3233λp.
    3334let l3 : label ≝ an_identifier … (p1 one) in
     
    3637   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
    3738   〈Some ? l3, GOTO ? l3〉 ] in
    38 mk_joint_internal_function LIN (prog_var_names … p)
     39mk_joint_internal_function LIN (prog_names … p)
    3940  (mk_universe … (p0 (p0 one)))
    4041  (mk_universe … one)
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3014 r3037  
    3838call_kind → unit → state_pc LTL_LIN_state → res(state LTL_LIN_state) ≝
    3939λk.λ_.λst. match k with
    40 [ PTR ⇒ return (st_no_pc … st)
     40[ PTR ⇒
     41  ! v ← Byte_of_val BadFunction
     42    (hwreg_retrieve (regs … st) RegisterA) ;
     43  if eq_bv … v (bv_zero …) then return (st_no_pc … st)
     44  else Error … [MSG BadFunction; MSG BadPointer]
    4145| ID ⇒ push_ra … st (pc … st)
    4246].
Note: See TracChangeset for help on using the changeset viewer.