Ignore:
Timestamp:
Mar 29, 2013, 12:38:41 PM (7 years ago)
Author:
campbell
Message:

Tidy up RTLabs preclassified_system definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_classified_system.ma

    r2811 r3031  
    1 (**************************************************************************)
    2 (*       ___                                                              *)
    3 (*      ||M||                                                             *)
    4 (*      ||A||       A project by Andrea Asperti                           *)
    5 (*      ||T||                                                             *)
    6 (*      ||I||       Developers:                                           *)
    7 (*      ||T||         The HELM team.                                      *)
    8 (*      ||A||         http://helm.cs.unibo.it                             *)
    9 (*      \   /                                                             *)
    10 (*       \ /        This file is distributed under the terms of the       *)
    11 (*        v         GNU General Public License Version 2                  *)
    12 (*                                                                        *)
    13 (**************************************************************************)
    141
    152include "RTLabs/RTLabs_abstract.ma".
    163include "RTLabs/RTLabs_semantics.ma".
    174include "common/Measurable.ma".
     5
     6(* First, plain RTLabs.  This for for the front-end, the back-end will get a
     7   prefix for its structured trace in terms of the version with the shadow
     8   stack below. *)
    189
    1910definition RTLabs_stack_ident :
     
    3728  (λ_.RTLabs_classify)
    3829  RTLabs_stack_ident.
     30
     31(* Now the version extended with a shadow stack.  This is the one the back-end
     32   will see, because it matches the RTLabs abstract status for the
     33   structured traces. *)
     34
     35definition RTLabs_ext_pcs ≝ mk_preclassified_system
     36  RTLabs_ext_fullexec
     37  (λg,s. RTLabs_cost (Ras_state … s))
     38  (λg,s. RTLabs_classify (Ras_state … s))
     39  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
Note: See TracChangeset for help on using the changeset viewer.