Changeset 2975


Ignore:
Timestamp:
Mar 27, 2013, 4:07:02 PM (4 years ago)
Author:
tranquil
Message:
  • RTL premain fixed
  • fixed bug in back end ops (subtracting to a porinter was reversed)
  • fixed globals initialization in LINToASM
Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2963 r2975  
    415415  let nxt_dptr ≝ dptr + size_init_data data in
    416416  〈nxt_dptr, do_store_init_data … u nxt_dptr data @ acc〉 in
     417〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … start_dptr)〉))))〉 ::
    417418\snd (foldr ?? f 〈start_dptr, [ ]〉 data).
    418419
  • src/RTL/RTL.ma

    r2955 r2975  
    113113  res in
    114114let res ≝ add_graph … l2
    115   (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] [ ]) l3)
     115  (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] rs) l3)
    116116  res in
    117117let res ≝ add_graph … l3
     
    128128| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
    129129| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
    130 | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     130| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct try @I
     131  try % try % try % try % try % whd /2 by double_lt3/
    131132| %{l2} %{(init_cost_label … p)} %
    132133]
  • src/common/BackEndOps.ma

    r2926 r2975  
    151151        else
    152152          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
    153           let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
     153          let 〈rslt,carry〉 ≝ op2 eval false op (\snd o1o0) b2 in
    154154          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
    155155          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
Note: See TracChangeset for help on using the changeset viewer.