Changeset 2484 for src/joint/Traces.ma


Ignore:
Timestamp:
Nov 22, 2012, 6:40:31 PM (8 years ago)
Author:
piccolo
Message:

fixed Traces and semantics
added commutation record (not yet finished) and proofs in lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2481 r2484  
    8282  let main ≝ prog_main … p in
    8383  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
    84   let st0' ≝ set_sp … spp st0 in
    8584  (* use exit sem_globals as ra and call_dest_for_main as dest *)
    86   ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
     85  let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
     86  ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
    8787  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    8888  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
Note: See TracChangeset for help on using the changeset viewer.