Changeset 1148


Ignore:
Timestamp:
Aug 30, 2011, 4:14:50 PM (8 years ago)
Author:
sacerdot
Message:

Function call/return finished (up to retrieving parameters from the stack
for external functions).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1146 r1148  
    176176
    177177(*CSC: to be implemented *)
    178 axiom fetch_external_args: external_function → state → list val.
     178axiom fetch_external_args: external_function → state → res (list val).(* ≝
     179 λfn,st.
     180  let registerno ≝ ? fn in
     181  ! vs ←
     182   mmap …
     183    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
     184  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
     185  ?.*)
    179186
    180187(*CSC: to be implemented; fails if the first list is longer *)
     
    296303         ret ? 〈 E0, goto l' (set_locals locals st)〉
    297304      | External fn ⇒
    298         let params ≝ fetch_external_args fn st in
     305        ! params ← fetch_external_args fn st;
    299306        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    300307        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    311318      let pc ≝ address_of_address_chunks pcl pch in
    312319      ret ? 〈E0,set_pc pc st〉
    313   | _ ⇒ ? ]
    314 (*
    315   ]
    316 | Returnstate v dst fs m ⇒
    317     match fs with
    318     [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    319     | cons f fs' ⇒
    320        ! locals ←
    321          mfold_left2 ???
    322           (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
    323         ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
    324     ]
    325 ]*).
     320  | _ ⇒ ? ].
    326321
    327322axiom WrongReturnValueType: String.
Note: See TracChangeset for help on using the changeset viewer.