Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (6 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTL_semantics.ml

    r2890 r2933  
    436436          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
    437437          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
    438           let st0 =
    439             Util.foldl (fun st0 reg_val ->
    440               rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st
    441               reg_vals
    442           in
    443438          Monad.m_bind0 (Monad.max_def Errors.res0)
    444             (Obj.magic (Joint_semantics.sp rTL_state_params st0)) (fun sp ->
     439            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
    445440            let st1 =
    446441              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
     
    449444                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
    450445                    (Joint_semantics.set_m rTL_state_params
    451                       (GenMem.free st0.Joint_semantics.m
    452                         (Types.pi1 sp).Pointers.pblock) st0)))
     446                      (GenMem.free st.Joint_semantics.m
     447                        (Types.pi1 sp).Pointers.pblock) st)))
    453448            in
    454449            let pc = hd.fr_pc in
     450          let st1 =
     451            Util.foldl (fun st0 reg_val ->
     452prerr_endline ("SALVO IL REGISTRO: r_" ^ string_of_int (Glue.int_of_matitapos reg_val.Types.fst));
     453              rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st1
     454              reg_vals
     455          in
    455456            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
    456457              Types.snd = pc }))))
Note: See TracChangeset for help on using the changeset viewer.