Changeset 3032


Ignore:
Timestamp:
Mar 29, 2013, 12:51:50 PM (4 years ago)
Author:
campbell
Message:

Remind myself why ms_rel_normal is reasonable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r3007 r3032  
    4141  (* It's tempting to have a general result that states in the relation always
    4242     have the same classification, but this may not be true when the step for
    43      s1 "disappears" in s2. *)
     43     s1 "disappears" in s2.  The best we can do is match calls, returns and
     44     "normal" steps (above), because while we may switch cl_other and cl_jump,
     45     nothing ever collapses into a cl_call or cl_return because they are always
     46     preceeded by the corresponding instruction. *)
    4447  ms_rel_classify_call : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_call → pcs_classify ms_C2 g2 s2 = cl_call;
    4548  ms_rel_classify_return : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_return → pcs_classify ms_C2 g2 s2 = cl_return;
Note: See TracChangeset for help on using the changeset viewer.