Changeset 1389 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Oct 17, 2011, 11:23:18 AM (8 years ago)
Author:
sacerdot
Message:

One more axiom closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1388 r1389  
    7171axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
    7272
    73 (*CSC: XXXX *)
    74 axiom framesize: list ident → state ertl_sem_params → res nat. (* ≝
    75   λglobals: list ident.
    76   λst.
    77    do f ← fetch_function globals st ;
    78    OK ? (joint_if_stacksize globals … f).*)
     73definition framesize:
     74 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝
     75  λglobals,ge,st.
     76   do f ← graph_fetch_function … ge st ;
     77   OK ? (joint_if_stacksize globals … f).
    7978
    8079definition get_hwsp : state ertl_sem_params → res address ≝
     
    9897  match stm with
    9998   [ ertl_st_ext_new_frame ⇒
    100       ! v ← framesize globals st;
     99      ! v ← framesize globals … ge st;
    101100      ! sp ← get_hwsp st;
    102101      ! newsp ← addr_sub sp v;
     
    104103        ret ? 〈E0,goto … l st〉
    105104   | ertl_st_ext_del_frame ⇒
    106       ! v ← framesize globals st;
     105      ! v ← framesize … ge st;
    107106      ! sp ← get_hwsp st;
    108107      ! newsp ← addr_add sp v;
     
    110109        ret ? 〈E0,goto … l st〉
    111110   | ertl_st_ext_frame_size dst ⇒
    112       ! v ← framesize globals st;
     111      ! v ← framesize … ge st;
    113112      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
    114113        ret ? 〈E0, goto … l st〉
Note: See TracChangeset for help on using the changeset viewer.