Ignore:
Timestamp:
Feb 21, 2012, 11:58:12 AM (8 years ago)
Author:
campbell
Message:

Add a distinguished final state to the front-end languages to match up
with the structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1672 r1713  
    511511  ] 
    512512| #v #k' #m' whd in ⊢ (?????%); cases k'; //;
    513     #r #f #e #k whd in ⊢ (?????%); cases r;
    514   [ whd; @step_returnstate_0
    515   | #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty
    516     @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //;
    517   ]
     513  [ whd in ⊢ (?????%); cases v // * //
     514  | #r #f #e #k whd in ⊢ (?????%); cases r //
     515    * * #b #ofs #ty
     516    @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //
     517    ]
     518| //
    518519]
    519520qed.
     
    536537  [ whd; %
    537538  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
    538       [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ] normalize
    539 (*      whd in ⊢ (? → ?????(??????%?)); *)
    540       cases m; #mc #mn #mp #Hstep normalize
    541 (*      whd in ⊢ (?????(??????%?));*)
     539      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m | #r ] normalize
     540      [ 1,2,3: cases m; #mc #mn #mp ] #Hstep normalize
    542541      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
    543       whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ]
     542      whd; @(star_step ????????? Hsteps) [ 2,5,8,11: @Hstep | 3,6,9,12: // ]
    544543  ]
    545544qed.
    546545
    547546lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
    548 * [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct %
    549                             | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct
    550                             ]
    551             | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct
    552             ]
    553   | *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct
     547* [ 4: #r #r' normalize #E destruct %
     548  | *: normalize #x1 #x2 #x3 #x4 #x5 try #x6 try #x7 destruct
    554549  ] qed.
Note: See TracChangeset for help on using the changeset viewer.