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

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr_semantics.ma

    r2666 r2783  
    55
    66definition ertlptr_save_frame:
    7  call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
    8  λk.λ_.λid.λst.
    9  do st ← match k with [ID ⇒ push_ra … st (pc … st) |
    10  PTR ⇒ return (st_no_pc … st)] ; OK …
    11    (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
    12     (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
     7 call_kind → unit  → state_pc ERTL_state → res (state … ERTL_state) ≝
     8 λk.λ_.λst.
     9 ! st' ← match k with
     10  [ ID ⇒ push_ra … st (pc … st)
     11  | PTR ⇒ return (st : state ?)
     12  ] ;
     13 ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
     14  return
     15   (set_frms ERTL_state (〈\fst (regs ERTL_state st'), pc_block (pc … st)〉 :: frms)
     16    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    1317
    1418definition eval_ertlptr_seq:
     
    5357     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    5458  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
    55   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     59  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
     60 
    5661definition ERTLptr_semantics ≝
    57   make_sem_graph_params ERTLptr ERTLptr_sem_uns.
     62  mk_sem_graph_params ERTLptr ERTLptr_sem_uns.
Note: See TracChangeset for help on using the changeset viewer.