Changeset 1295


Ignore:
Timestamp:
Oct 5, 2011, 4:15:20 PM (8 years ago)
Author:
sacerdot
Message:

More progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1294 r1295  
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1010
    11 (*CSC: XXXX *)
    12 axiom rtl_succ_p: label → address → address.
     11(*CSC: XXXX; we need to create a brand new chunk per label, so that
     12  pointer operations on labels are not semantically valid!! *)
    1313axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
     14
     15(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
     16  Maybe there is a better way to organize the code!!! *)
     17definition rtl_succ_p: label → address → address.
     18 #l #_ generalize in match (refl … (beval_pair_of_pointer (rtl_pointer_of_label l)))
     19 cases (beval_pair_of_pointer (rtl_pointer_of_label l)) in ⊢ (???% → ?)
     20  [ #res #_ @res
     21  | #msg cases (rtl_pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
     22qed.
    1423
    1524axiom rtl_pop_frame: unit → res unit.
     
    3645axiom rtl_init_locals : list register → register_env beval.
    3746axiom rtl_fetch_statement: ∀globals. state rtl_sem_params → res (rtl_statement globals).
     47
    3848axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
    3949
Note: See TracChangeset for help on using the changeset viewer.