Changeset 2538 for src/joint


Ignore:
Timestamp:
Dec 6, 2012, 1:39:23 PM (7 years ago)
Author:
tranquil
Message:

fixed Traces.ma after changes in joint/semantics.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2529 r2538  
    8686  (* use exit sem_globals as ra and call_dest_for_main as dest *)
    8787  let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
    88   ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
     88  ! st0'' ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
    8989  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    90   ! bl ← block_of_call … ge st_pc0 (inl … main) ;
     90  ! bl ← block_of_call … ge (inl … main) st_pc0;
    9191  ! 〈i, fn〉 ← fetch_function … ge bl ;
    9292  match fn with
    9393  [ Internal ifn ⇒
    94     ! st' ← eval_internal_call_no_pc … ge i ifn (call_args_for_main … pars) st_pc0 ;
     94    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st_pc0 ;
    9595    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    9696    return mk_state_pc … st' pc'
     
    103103  match stmt with
    104104  [ CALL f args dest ⇒
    105     match (! bl ← block_of_call … (ev_genv p) st f ;
     105    match (! bl ← block_of_call … (ev_genv p) f st ;
    106106            fetch_function … (ev_genv p) bl) with
    107107    [ OK id_fn ⇒
     
    140140    [ sequential s _ ⇒ joint_classify_step p st s
    141141    | final s ⇒ joint_classify_final p s
     142    | FCOND _ _ _ _ ⇒ cl_jump
    142143    ]
    143144  | Error _ ⇒ cl_other
     
    182183  fetch_statement … (ev_genv p) (pc … st) =
    183184    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
    184   block_of_call … (ev_genv p) st f' = OK ? bl ∧
     185  block_of_call … (ev_genv p) f' st = OK ? bl ∧
    185186  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
    186187#p #st
     
    188189inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta
    189190[2: #e #_ #ABS destruct(ABS) ]
    190 * #i_f * [2: * [ #lbl | | #fl #f #args ] #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     191* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
     192  normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    191193@cond_call_other
    192194[ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
     
    267269      [ CALL f' args dest ⇒
    268270        match
    269           (! bl ← block_of_call … (ev_genv p) st f' ;
     271          (! bl ← block_of_call … (ev_genv p) f' st;
    270272           fetch_internal_function … (ev_genv p) bl) with
    271273        [ OK i_f ⇒ \fst i_f
     
    341343   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    342344   (* as_call_ident ≝ *) (joint_call_ident p).
    343 
Note: See TracChangeset for help on using the changeset viewer.