source: driver/extracted/stacksize.mli @ 3106

Last change on this file since 3106 was 2951, checked in by sacerdot, 7 years ago

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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