extracted/clight_classified_system.ml

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