Ignore:
Timestamp:
Jan 23, 2012, 5:37:26 PM (8 years ago)
Author:
campbell
Message:

Corrections to structured trace definitions (see the mailing list).
Also update RTLabs work to match.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1652 r1654  
    4343          trace_label_label S ends_flag start_status end_status
    4444with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
     45  (* Single steps within a function which reach a label.
     46     Note that this is the only case applicable for a jump. *)
    4547  | tal_base_not_return:
    4648      ∀start_status: S.
    4749      ∀final_status: S.
    4850        as_execute S start_status final_status →
    49         ¬ as_classifier S start_status cl_return →
     51        (as_classifier S start_status cl_jump ∨
     52         as_classifier S start_status cl_other) →
    5053        as_costed S final_status →
    5154          trace_any_label S doesnt_end_with_ret start_status final_status
     
    5659        as_classifier S start_status cl_return →
    5760          trace_any_label S ends_with_ret start_status final_status
     61  (* A call followed by a label on return. *)
     62  | tal_base_call:
     63      ∀status_pre_fun_call: S.
     64      ∀status_start_fun_call: S.
     65      ∀status_final: S.
     66        as_execute S status_pre_fun_call status_start_fun_call →
     67        ∀H:as_classifier S status_pre_fun_call cl_call.
     68          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
     69          trace_label_return S status_start_fun_call status_final →
     70          as_costed S status_final →
     71            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
     72  (* A call followed by a non-empty trace. *)
    5873  | tal_step_call:
    5974      ∀end_flag: trace_ends_with_ret.
     
    6681          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    6782          trace_label_return S status_start_fun_call status_after_fun_call →
     83          ¬ as_costed S status_after_fun_call →
    6884          trace_any_label S end_flag status_after_fun_call status_final →
    6985            trace_any_label S end_flag status_pre_fun_call status_final
     
    120136          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    121137          trace_label_return S status_start_fun_call status_after_fun_call →
     138          ¬ as_costed S status_after_fun_call →
    122139          trace_any_call S status_after_fun_call status_final →
    123140            trace_any_call S status_pre_fun_call status_final
     
    137154[ tal_base_not_return start final _ _ C ⇒ C
    138155| tal_base_return _ _  _ _ ⇒ I
    139 | tal_step_call f pre start after final X C RET LR tr' ⇒ trace_any_label_label … tr'
     156| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     157| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    140158| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    141159].
Note: See TracChangeset for help on using the changeset viewer.