Changeset 1902 for src/common
- Timestamp:
- Apr 26, 2012, 4:20:32 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/StructuredTraces.ma
r1901 r1902 15 15 as_classifier : as_status → status_class → Prop; 16 16 as_costed : as_status → Prop; 17 as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop; 18 as_program_counters_properly_related: as_status → as_status → Prop 17 as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop 19 18 }. 20 19 … … 71 70 trace_label_return S status_start_fun_call status_final → 72 71 as_costed S status_final → 73 as_program_counters_properly_related S status_pre_fun_call status_final →74 72 trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final 75 73 (* A call followed by a non-empty trace. *) … … 85 83 trace_label_return S status_start_fun_call status_after_fun_call → 86 84 ¬ as_costed S status_after_fun_call → 87 as_program_counters_properly_related S status_pre_fun_call status_after_fun_call →88 85 trace_any_label S end_flag status_after_fun_call status_final → 89 86 trace_any_label S end_flag status_pre_fun_call status_final … … 219 216 [ tal_base_not_return start final _ _ C ⇒ C 220 217 | tal_base_return _ _ _ _ ⇒ I 221 | tal_base_call _ _ _ _ _ _ _ C _⇒ C222 | tal_step_call f pre start after final X C RET PROPERLR C' tr' ⇒ trace_any_label_label … tr'218 | tal_base_call _ _ _ _ _ _ _ C ⇒ C 219 | tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr' 223 220 | tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr' 224 221 ].
Note: See TracChangeset
for help on using the changeset viewer.