Ignore:
Timestamp:
Oct 17, 2011, 1:40:13 AM (9 years ago)
Author:
sacerdot
Message:
  1. fetch_result and pop_frame now takes the genv in input
  2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1384 r1385  
    5252
    5353 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    54  ; pop_frame: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
    5554   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    5655     type of arguments. To be fixed using a dependent type *)
     
    7675
    7776 ; fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address)
    78  ; fetch_result: state (mk_sem_params … more_sparams1) → res (list beval)
     77 ; fetch_result: genv globals p → state (mk_sem_params … more_sparams1) → res (list beval)
     78
     79 ; pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)))
    7980
    8081 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val)
     
    341342    | RETURN ⇒
    342343      ! 〈st,ra〉 ← fetch_ra … st;
    343       ! st ← pop_frame … st;
     344      ! st ← pop_frame … ge st;
    344345        ret ? 〈E0,set_pc … ra st〉].
    345346cases addr //
     
    353354      do 〈st,ra〉 ← fetch_ra … st;
    354355      if eq_address ra exit then
    355        do vals ← fetch_result … st ;
     356       do vals ← fetch_result … ge st ;
    356357       Word_of_list_beval vals
    357358      else
Note: See TracChangeset for help on using the changeset viewer.