- Mar 29, 2013, 12:51:50 PM (4 years ago)
- 1 edited
r3007 r3032 41 41 (* It's tempting to have a general result that states in the relation always 42 42 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. *) 44 47 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; 45 48 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.