Changeset 2802 for src


Ignore:
Timestamp:
Mar 7, 2013, 1:53:23 PM (7 years ago)
Author:
sacerdot
Message:

New file Clight_classified_system with the classified system for Clight.
The code comes from correctness.ma and it is used in the untrusted code
for debugging too.

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2774 r2802  
    3636
    3737
    38 include "Clight/Clight_abstract.ma".
    39 include "common/Measurable.ma".
    40 
    41 definition Clight_stack_ident :
    42   cl_genv →
    43   ∀s:Clight_state.
    44   match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
    45   ident ≝
    46 λge,s.
    47 match s return λs. match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
    48 [ Callstate id _ _ _ _ ⇒ λ_. id
    49 | _ ⇒ λH.⊥
    50 ].
    51 @H
    52 qed.
    53 
    54 definition Clight_pcs : preclassified_system ≝
    55 mk_preclassified_system
    56   clight_fullexec
    57   (λ_.Clight_labelled)
    58   (λ_.Clight_classify)
    59   Clight_stack_ident.
     38include "Clight/Clight_classified_system.ma".
    6039
    6140(* From measurable on Clight, we will end up with an RTLabs flat trace where
Note: See TracChangeset for help on using the changeset viewer.