extracted/rTLabs_classified_system.ml

   1 open Preamble
   2
   3 open Deqsets_extra
   4
   5 open CostSpec
   6
   7 open Sets
   8
   9 open Listb
  10
  11 open StructuredTraces
  12
  13 open BitVectorTrie
  14
  15 open Graphs
  16
  17 open Order
  18
  19 open Registers
  20
  21 open FrontEndOps
  22
  23 open RTLabs_syntax
  24
  25 open SmallstepExec
  26
  27 open CostLabel
  28
  29 open Events
  30
  31 open IOMonad
  32
  33 open IO
  34
  35 open Extra_bool
  36
  37 open Coqlib
  38
  39 open Values
  40
  41 open FrontEndVal
  42
  43 open Hide
  44
  45 open ByteValues
  46
  47 open Division
  48
  49 open Z
  50
  51 open BitVectorZ
  52
  53 open Pointers
  54
  55 open GenMem
  56
  57 open FrontEndMem
  58
  59 open Proper
  60
  61 open PositiveMap
  62
  63 open Deqsets
  64
  65 open Extralib
  66
  67 open Lists
  68
  69 open Identifiers
  70
  71 open Exp
  72
  73 open Arithmetic
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Util
  80
  81 open FoldStuff
  82
  83 open BitVector
  84
  85 open Extranat
  86
  87 open Integers
  88
  89 open AST
  90
  91 open Globalenvs
  92
  93 open ErrorMessages
  94
  95 open Option
  96
  97 open Setoids
  98
  99 open Monad
 100
 101 open Jmeq
 102
 103 open Russell
 104
 105 open Positive
 106
 107 open PreIdentifiers
 108
 109 open Errors
 110
 111 open Bool
 112
 113 open Relations
 114
 115 open Nat
 116
 117 open Hints_declaration
 118
 119 open Core_notation
 120
 121 open Pts
 122
 123 open Logic
 124
 125 open Types
 126
 127 open List
 128
 129 open RTLabs_semantics
 130
 131 open RTLabs_abstract
 132
 133 open Stacksize
 134
 135 open Executions
 136
 137 open Measurable
 138
 139 (** val rTLabs_stack_ident :
 140     RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_state -> AST.ident **)
 141 let rTLabs_stack_ident ge s =
 142   (match s with
 143    | RTLabs_semantics.State (x, x0, x1) ->
 144      (fun _ -> assert false (* absurd case *))
 145    | RTLabs_semantics.Callstate (id, x, x0, x1, x2, x3) -> (fun _ -> id)
 146    | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
 147      (fun _ -> assert false (* absurd case *))
 148    | RTLabs_semantics.Finalstate x ->
 149      (fun _ -> assert false (* absurd case *))) __
 150
 151 (** val rTLabs_pcs : Measurable.preclassified_system **)
 152 let rTLabs_pcs =
 153   { Measurable.pcs_exec = RTLabs_semantics.rTLabs_fullexec;
 154     Measurable.pcs_labelled = (fun x ->
 155     Obj.magic RTLabs_abstract.rTLabs_cost); Measurable.pcs_classify =
 156     (fun x -> Obj.magic RTLabs_abstract.rTLabs_classify);
 157     Measurable.pcs_callee =
 158     (Obj.magic (fun x x0 _ -> rTLabs_stack_ident x x0)) }
 159
 160 (** val rTLabs_ext_pcs : Measurable.preclassified_system **)
 161 let rTLabs_ext_pcs =
 162   { Measurable.pcs_exec = RTLabs_abstract.rTLabs_ext_fullexec;
 163     Measurable.pcs_labelled = (fun g s ->
 164     RTLabs_abstract.rTLabs_cost (Obj.magic s).RTLabs_abstract.ras_state);
 165     Measurable.pcs_classify = (fun g s ->
 166     RTLabs_abstract.rTLabs_classify (Obj.magic s).RTLabs_abstract.ras_state);
 167     Measurable.pcs_callee = (fun g s _ ->
 168     rTLabs_stack_ident (Obj.magic g) (Obj.magic s).RTLabs_abstract.ras_state) }
 169