Changeset 1583 for src/common


Ignore:
Timestamp:
Dec 2, 2011, 1:02:08 PM (8 years ago)
Author:
campbell
Message:

More on RTLabs structured traces.
Fixed mistake in structure trace definition that made it unhabitable.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1545 r1583  
    549549  ?*)
    550550.
     551
     552lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
     553  find_funct Genv F ge v = Some F f →
     554  ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset)  ∧ find_funct_ptr Genv F ge b = Some F f.
     555#F #ge *
     556[ #f #E normalize in E; destruct
     557| #sz #i #f #E normalize in E; destruct
     558| #f #fn #E normalize in E; destruct
     559| #r #f #E normalize in E; destruct
     560| * #pty #b #c * #off #f #E normalize in E;
     561  cases off in E ⊢ %; [ 2,3: #x ]
     562  #E normalize in E; destruct
     563  %{pty} %{b} %{c} % // @E
     564] qed.
     565
    551566(*
    552567##[ #A B C transf p b f; elim p; #fns main vars;
  • src/common/StructuredTraces.ma

    r1574 r1583  
    7676        trace_any_label S end_flag status_init status_end →
    7777        as_classifier S status_pre cl_other →
    78         ¬ (as_costed S status_pre) →
     78        ¬ (as_costed S status_init) →
    7979          trace_any_label S end_flag status_pre status_end.
    8080
Note: See TracChangeset for help on using the changeset viewer.