extracted/cminor_classified_system.ml

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