Changeset 1713 for src/Clight/Csem.ma


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/Csem.ma

    r1672 r1713  
    956956      ∀res: val.
    957957      ∀k: cont.
    958       ∀m: mem. state.
     958      ∀m: mem. state
     959  | Finalstate:
     960      ∀r: int.
     961      state.
    959962                 
    960963(* * Find the statement and manufacture the continuation
     
    11961199  | step_cost: ∀f,lbl,s,k,e,m.
    11971200      step ge (State f (Scost lbl s) k e m)
    1198            (Echarge lbl) (State f s k e m).
     1201           (Echarge lbl) (State f s k e m)
     1202 
     1203  | step_final: ∀r,m.
     1204      step ge (Returnstate (Vint I32 r) Kstop m)
     1205           E0 (Finalstate r).
    11991206
    12001207(*
     
    12201227
    12211228inductive final_state: state -> int -> Prop :=
    1222   | final_state_intro: ∀r,m.
    1223       final_state (Returnstate (Vint I32 r) Kstop m) r.
     1229  | final_state_intro: ∀r.
     1230      final_state (Finalstate r) r.
    12241231
    12251232(* * Execution of a whole program: [exec_program p beh]
Note: See TracChangeset for help on using the changeset viewer.