extracted/clight_abstract.ml

   1 open Preamble
   2
   3 open TypeComparison
   4
   5 open ClassifyOp
   6
   7 open Events
   8
   9 open Smallstep
  10
  11 open CostLabel
  12
  13 open Csyntax
  14
  15 open Extra_bool
  16
  17 open Coqlib
  18
  19 open Values
  20
  21 open FrontEndVal
  22
  23 open Hide
  24
  25 open ByteValues
  26
  27 open Division
  28
  29 open Z
  30
  31 open BitVectorZ
  32
  33 open Pointers
  34
  35 open GenMem
  36
  37 open FrontEndMem
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open Extralib
  46
  47 open Lists
  48
  49 open Identifiers
  50
  51 open Exp
  52
  53 open Arithmetic
  54
  55 open Vector
  56
  57 open Div_and_mod
  58
  59 open Util
  60
  61 open FoldStuff
  62
  63 open BitVector
  64
  65 open Extranat
  66
  67 open Integers
  68
  69 open AST
  70
  71 open ErrorMessages
  72
  73 open Option
  74
  75 open Setoids
  76
  77 open Monad
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open Positive
  84
  85 open PreIdentifiers
  86
  87 open Bool
  88
  89 open Relations
  90
  91 open Nat
  92
  93 open List
  94
  95 open Hints_declaration
  96
  97 open Core_notation
  98
  99 open Pts
 100
 101 open Logic
 102
 103 open Types
 104
 105 open Errors
 106
 107 open Globalenvs
 108
 109 open Csem
 110
 111 (** val clight_labelled : Csem.state -> Bool.bool **)
 112 let clight_labelled = function
 113 | Csem.State (f, s0, k, e, m) ->
 114   (match s0 with
 115    | Csyntax.Sskip -> Bool.False
 116    | Csyntax.Sassign (x, x0) -> Bool.False
 117    | Csyntax.Scall (x, x0, x1) -> Bool.False
 118    | Csyntax.Ssequence (x, x0) -> Bool.False
 119    | Csyntax.Sifthenelse (x, x0, x1) -> Bool.False
 120    | Csyntax.Swhile (x, x0) -> Bool.False
 121    | Csyntax.Sdowhile (x, x0) -> Bool.False
 122    | Csyntax.Sfor (x, x0, x1, x2) -> Bool.False
 123    | Csyntax.Sbreak -> Bool.False
 124    | Csyntax.Scontinue -> Bool.False
 125    | Csyntax.Sreturn x -> Bool.False
 126    | Csyntax.Sswitch (x, x0) -> Bool.False
 127    | Csyntax.Slabel (x, x0) -> Bool.False
 128    | Csyntax.Sgoto x -> Bool.False
 129    | Csyntax.Scost (x, x0) -> Bool.True)
 130 | Csem.Callstate (x, x0, x1, x2, x3) -> Bool.False
 131 | Csem.Returnstate (x, x0, x1) -> Bool.False
 132 | Csem.Finalstate x -> Bool.False
 133
 134 open IOMonad
 135
 136 open IO
 137
 138 open Sets
 139
 140 open Listb
 141
 142 open StructuredTraces
 143
 144 (** val clight_classify : Csem.state -> StructuredTraces.status_class **)
 145 let clight_classify = function
 146 | Csem.State (x, x0, x1, x2, x3) -> StructuredTraces.Cl_other
 147 | Csem.Callstate (x, x0, x1, x2, x3) -> StructuredTraces.Cl_call
 148 | Csem.Returnstate (x, x0, x1) -> StructuredTraces.Cl_return
 149 | Csem.Finalstate x -> StructuredTraces.Cl_other
 150
 151 type clight_state = Csem.state
 152
 153 type cl_genv = Csem.genv
 154
 155 type cl_env = Csem.env
 156
 157 type cl_cont = Csem.cont
 158
 159 (** val clState :
 160     Csyntax.function0 -> Csyntax.statement -> Csem.cont -> Csem.env ->
 161     GenMem.mem -> Csem.state **)
 162 let clState x x0 x1 x2 x3 =
 163   Csem.State (x, x0, x1, x2, x3)
 164
 165 (** val clReturnstate :
 166     Values.val0 -> Csem.cont -> GenMem.mem -> Csem.state **)
 167 let clReturnstate x x0 x1 =
 168   Csem.Returnstate (x, x0, x1)
 169
 170 (** val clCallstate :
 171     AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list -> Csem.cont
 172     -> GenMem.mem -> Csem.state **)
 173 let clCallstate x x0 x1 x2 x3 =
 174   Csem.Callstate (x, x0, x1, x2, x3)
 175
 176 (** val clKseq : Csyntax.statement -> Csem.cont -> Csem.cont **)
 177 let clKseq x x0 =
 178   Csem.Kseq (x, x0)
 179