extracted/clight_abstract.mli

   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
 113 open IOMonad
 114
 115 open IO
 116
 117 open Sets
 118
 119 open Listb
 120
 121 open StructuredTraces
 122
 123 val clight_classify : Csem.state -> StructuredTraces.status_class
 124
 125 type clight_state = Csem.state
 126
 127 type cl_genv = Csem.genv
 128
 129 type cl_env = Csem.env
 130
 131 type cl_cont = Csem.cont
 132
 133 val clState :
 134   Csyntax.function0 -> Csyntax.statement -> Csem.cont -> Csem.env ->
 135   GenMem.mem -> Csem.state
 136
 137 val clReturnstate : Values.val0 -> Csem.cont -> GenMem.mem -> Csem.state
 138
 139 val clCallstate :
 140   AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list -> Csem.cont ->
 141   GenMem.mem -> Csem.state
 142
 143 val clKseq : Csyntax.statement -> Csem.cont -> Csem.cont
 144