extracted/stacksize.mli

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open Hide
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Extranat
  34
  35 open Vector
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Z
  42
  43 open BitVectorZ
  44
  45 open Pointers
  46
  47 open Coqlib
  48
  49 open Values
  50
  51 open Events
  52
  53 open IOMonad
  54
  55 open IO
  56
  57 open Sets
  58
  59 open Listb
  60
  61 open Proper
  62
  63 open PositiveMap
  64
  65 open Deqsets
  66
  67 open ErrorMessages
  68
  69 open PreIdentifiers
  70
  71 open Errors
  72
  73 open Extralib
  74
  75 open Setoids
  76
  77 open Monad
  78
  79 open Option
  80
  81 open Div_and_mod
  82
  83 open Russell
  84
  85 open Util
  86
  87 open Lists
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open Jmeq
  96
  97 open StructuredTraces
  98
  99 type call_ud =
 100 | Up of AST.ident
 101 | Down of AST.ident
 102
 103 val call_ud_rect_Type4 :
 104   (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
 105
 106 val call_ud_rect_Type5 :
 107   (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
 108
 109 val call_ud_rect_Type3 :
 110   (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
 111
 112 val call_ud_rect_Type2 :
 113   (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
 114
 115 val call_ud_rect_Type1 :
 116   (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
 117
 118 val call_ud_rect_Type0 :
 119   (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
 120
 121 val call_ud_inv_rect_Type4 :
 122   call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
 123
 124 val call_ud_inv_rect_Type3 :
 125   call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
 126
 127 val call_ud_inv_rect_Type2 :
 128   call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
 129
 130 val call_ud_inv_rect_Type1 :
 131   call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
 132
 133 val call_ud_inv_rect_Type0 :
 134   call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
 135
 136 val call_ud_discr : call_ud -> call_ud -> __
 137
 138 val call_ud_jmdiscr : call_ud -> call_ud -> __
 139
 140 type stacksize_info = { current : Nat.nat; maximum : Nat.nat }
 141
 142 val stacksize_info_rect_Type4 :
 143   (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
 144
 145 val stacksize_info_rect_Type5 :
 146   (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
 147
 148 val stacksize_info_rect_Type3 :
 149   (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
 150
 151 val stacksize_info_rect_Type2 :
 152   (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
 153
 154 val stacksize_info_rect_Type1 :
 155   (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
 156
 157 val stacksize_info_rect_Type0 :
 158   (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
 159
 160 val current : stacksize_info -> Nat.nat
 161
 162 val maximum : stacksize_info -> Nat.nat
 163
 164 val stacksize_info_inv_rect_Type4 :
 165   stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
 166
 167 val stacksize_info_inv_rect_Type3 :
 168   stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
 169
 170 val stacksize_info_inv_rect_Type2 :
 171   stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
 172
 173 val stacksize_info_inv_rect_Type1 :
 174   stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
 175
 176 val stacksize_info_inv_rect_Type0 :
 177   stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
 178
 179 val stacksize_info_discr : stacksize_info -> stacksize_info -> __
 180
 181 val stacksize_info_jmdiscr : stacksize_info -> stacksize_info -> __
 182
 183 val update_stacksize_info :
 184   (AST.ident -> Nat.nat Types.option) -> stacksize_info -> call_ud List.list
 185   -> stacksize_info
 186
 187 val extract_call_ud_from_observables :
 188   StructuredTraces.intensional_event List.list -> call_ud List.list
 189
 190 val extract_call_ud_from_tlr :
 191   StructuredTraces.abstract_status -> __ -> __ ->
 192   StructuredTraces.trace_label_return -> AST.ident -> call_ud List.list
 193
 194 val extract_call_ud_from_tll :
 195   StructuredTraces.trace_ends_with_ret -> StructuredTraces.abstract_status ->
 196   __ -> __ -> StructuredTraces.trace_label_label -> AST.ident -> call_ud
 197   List.list
 198