source: src/LIN/semantics.ma @ 1408

Last change on this file since 1408 was 1408, checked in by sacerdot, 8 years ago
  1. Added joint/BEGlobalenvs that is a modification of common/Globalenvs where
    • the memory used is the back-end one
    • no lookup via values is implemented
    • global variables are never initialized in the back-end
  2. Added to all semantics some default value to initialize the initial state
  3. Initial state initialization (in joint/semantics.ma) almost completed.
File size: 1.0 KB
Line 
1include "LIN/joint_LTL_LIN_semantics.ma".
2include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
3
4definition lin_succ_pc: unit → address → res address :=
5 λ_.λaddr. addr_add addr 1.
6
7(*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *)
8axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
9
10(*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
11axiom BadProgramCounter: String.
12axiom lin_fetch_statement:
13 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).
14(* λglobals,ge,st.
15  do p ← pointer_of_address (pc … st) ;
16  let b ≝ pblock p in
17  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
18  [ Internal def' ⇒
19     let off ≝ poff p in
20     opt_to_res ? [MSG BadProgramCounter] (\snd (nth ?? (joint_if_code … def') off))
21  | External _ ⇒ Error … [MSG BadProgramCounter]].*)
22
23definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
Note: See TracBrowser for help on using the repository browser.