Changeset 2785 for src/joint


Ignore:
Timestamp:
Mar 6, 2013, 2:58:09 PM (7 years ago)
Author:
piccolo
Message:

Traces.ma repaired

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2783 r2785  
    7979(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8080  let main ≝ prog_main … p in
    81   let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
     81  let st0 ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m in
    8282  (* use exit_pc as ra and call_dest_for_main as dest *)
    8383  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
Note: See TracChangeset for help on using the changeset viewer.