71 open Hints_declaration
111 type env = Values.val0 Identifiers.identifier_map
113 type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
117 | Kseq of Cminor_syntax.stmt * cont
120 val cont_rect_Type4 :
121 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
124 val cont_rect_Type3 :
125 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
128 val cont_rect_Type2 :
129 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
132 val cont_rect_Type1 :
133 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
136 val cont_rect_Type0 :
137 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
140 val cont_inv_rect_Type4 :
141 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
142 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
144 val cont_inv_rect_Type3 :
145 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
146 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
148 val cont_inv_rect_Type2 :
149 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
150 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
152 val cont_inv_rect_Type1 :
153 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
154 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
156 val cont_inv_rect_Type0 :
157 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
158 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
160 val cont_discr : cont -> cont -> __
162 val cont_jmdiscr : cont -> cont -> __
166 | Scall of (AST.ident, AST.typ) Types.prod Types.option
167 * Cminor_syntax.internal_function * Pointers.block * env * cont *
170 val stack_rect_Type4 :
171 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
172 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
173 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
175 val stack_rect_Type3 :
176 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
177 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
178 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
180 val stack_rect_Type2 :
181 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
182 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
183 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
185 val stack_rect_Type1 :
186 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
187 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
188 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
190 val stack_rect_Type0 :
191 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
192 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
193 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
195 val stack_inv_rect_Type4 :
196 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
197 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
198 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
200 val stack_inv_rect_Type3 :
201 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
202 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
203 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
205 val stack_inv_rect_Type2 :
206 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
207 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
208 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
210 val stack_inv_rect_Type1 :
211 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
212 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
213 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
215 val stack_inv_rect_Type0 :
216 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
217 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
218 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
220 val stack_jmdiscr : stack -> stack -> __
223 | State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
224 * GenMem.mem * Pointers.block * cont * stack
225 | Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
226 * Values.val0 List.list * GenMem.mem * stack
227 | Returnstate of Values.val0 Types.option * GenMem.mem * stack
228 | Finalstate of Integers.int
230 val state_rect_Type4 :
231 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
232 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
233 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
234 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
235 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
237 val state_rect_Type5 :
238 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
239 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
240 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
241 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
242 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
244 val state_rect_Type3 :
245 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
246 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
247 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
248 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
249 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
251 val state_rect_Type2 :
252 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
253 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
254 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
255 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
256 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
258 val state_rect_Type1 :
259 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
260 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
261 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
262 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
263 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
265 val state_rect_Type0 :
266 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
267 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
268 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
269 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
270 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
272 val state_inv_rect_Type4 :
273 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
274 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
275 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
276 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
277 Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
280 val state_inv_rect_Type3 :
281 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
282 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
283 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
284 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
285 Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
288 val state_inv_rect_Type2 :
289 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
290 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
291 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
292 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
293 Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
296 val state_inv_rect_Type1 :
297 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
298 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
299 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
300 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
301 Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
304 val state_inv_rect_Type0 :
305 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
306 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
307 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
308 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
309 Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
312 val state_jmdiscr : state -> state -> __
315 genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
316 GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res
319 Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
320 Types.sig0 Errors.res
323 AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1 ->
327 PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
328 Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
329 Types.prod Types.sig0 Types.option
331 val find_label_always :
332 PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
333 Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
334 Types.prod Types.sig0
337 Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
338 Types.sig0 Errors.res
340 val init_locals : env -> (AST.ident, AST.typ) Types.prod List.list -> env
343 ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
344 -> (Events.trace, 'a2 List.list) Types.prod Errors.res
347 genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
350 val is_final : state -> Integers.int Types.option
352 val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
354 val make_global : Cminor_syntax.cminor_program -> genv
356 val make_initial_state : Cminor_syntax.cminor_program -> state Errors.res
358 val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
360 val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv
362 val make_initial_noinit_state :
363 Cminor_syntax.cminor_noinit_program -> state Errors.res
365 val cminor_noinit_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec