119 type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
121 type frame = { func : RTLabs_syntax.internal_function;
122 locals : Values.val0 Registers.register_env;
123 next : Graphs.label; sp : Pointers.block;
124 retdst : Registers.register Types.option }
126 val frame_rect_Type4 :
127 (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
128 Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
131 val frame_rect_Type5 :
132 (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
133 Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
136 val frame_rect_Type3 :
137 (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
138 Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
141 val frame_rect_Type2 :
142 (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
143 Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
146 val frame_rect_Type1 :
147 (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
148 Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
151 val frame_rect_Type0 :
152 (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
153 Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
156 val func : frame -> RTLabs_syntax.internal_function
158 val locals : frame -> Values.val0 Registers.register_env
160 val next : frame -> Graphs.label
162 val sp : frame -> Pointers.block
164 val retdst : frame -> Registers.register Types.option
166 val frame_inv_rect_Type4 :
167 frame -> (RTLabs_syntax.internal_function -> Values.val0
168 Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
169 Registers.register Types.option -> __ -> 'a1) -> 'a1
171 val frame_inv_rect_Type3 :
172 frame -> (RTLabs_syntax.internal_function -> Values.val0
173 Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
174 Registers.register Types.option -> __ -> 'a1) -> 'a1
176 val frame_inv_rect_Type2 :
177 frame -> (RTLabs_syntax.internal_function -> Values.val0
178 Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
179 Registers.register Types.option -> __ -> 'a1) -> 'a1
181 val frame_inv_rect_Type1 :
182 frame -> (RTLabs_syntax.internal_function -> Values.val0
183 Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
184 Registers.register Types.option -> __ -> 'a1) -> 'a1
186 val frame_inv_rect_Type0 :
187 frame -> (RTLabs_syntax.internal_function -> Values.val0
188 Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
189 Registers.register Types.option -> __ -> 'a1) -> 'a1
191 val frame_jmdiscr : frame -> frame -> __
193 val adv : Graphs.label -> frame -> frame
196 | State of frame * frame List.list * GenMem.mem
197 | Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
198 * Values.val0 List.list * Registers.register Types.option
199 * frame List.list * GenMem.mem
200 | Returnstate of Values.val0 Types.option * Registers.register Types.option
201 * frame List.list * GenMem.mem
202 | Finalstate of Integers.int
204 val state_rect_Type4 :
205 (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
206 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
207 Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
208 (Values.val0 Types.option -> Registers.register Types.option -> frame
209 List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
211 val state_rect_Type5 :
212 (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
213 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
214 Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
215 (Values.val0 Types.option -> Registers.register Types.option -> frame
216 List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
218 val state_rect_Type3 :
219 (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
220 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
221 Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
222 (Values.val0 Types.option -> Registers.register Types.option -> frame
223 List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
225 val state_rect_Type2 :
226 (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
227 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
228 Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
229 (Values.val0 Types.option -> Registers.register Types.option -> frame
230 List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
232 val state_rect_Type1 :
233 (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
234 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
235 Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
236 (Values.val0 Types.option -> Registers.register Types.option -> frame
237 List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
239 val state_rect_Type0 :
240 (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
241 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
242 Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
243 (Values.val0 Types.option -> Registers.register Types.option -> frame
244 List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
246 val state_inv_rect_Type4 :
247 state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
248 (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
249 List.list -> Registers.register Types.option -> frame List.list ->
250 GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
251 Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
252 (Integers.int -> __ -> 'a1) -> 'a1
254 val state_inv_rect_Type3 :
255 state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
256 (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
257 List.list -> Registers.register Types.option -> frame List.list ->
258 GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
259 Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
260 (Integers.int -> __ -> 'a1) -> 'a1
262 val state_inv_rect_Type2 :
263 state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
264 (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
265 List.list -> Registers.register Types.option -> frame List.list ->
266 GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
267 Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
268 (Integers.int -> __ -> 'a1) -> 'a1
270 val state_inv_rect_Type1 :
271 state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
272 (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
273 List.list -> Registers.register Types.option -> frame List.list ->
274 GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
275 Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
276 (Integers.int -> __ -> 'a1) -> 'a1
278 val state_inv_rect_Type0 :
279 state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
280 (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
281 List.list -> Registers.register Types.option -> frame List.list ->
282 GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
283 Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
284 (Integers.int -> __ -> 'a1) -> 'a1
286 val state_jmdiscr : state -> state -> __
289 frame -> frame List.list -> GenMem.mem -> Graphs.label -> state
291 val next_instruction : frame -> RTLabs_syntax.statement
294 (Registers.register, AST.typ) Types.prod List.list -> Values.val0
295 Registers.register_env
298 PreIdentifiers.identifier -> Values.val0 -> Values.val0
299 Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
303 (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list
304 -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env
308 Values.val0 Registers.register_env -> Registers.register -> Values.val0
312 genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
315 val rTLabs_is_final : state -> Integers.int Types.option
317 val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
319 val make_global : RTLabs_syntax.rTLabs_program -> genv
321 val make_initial_state : RTLabs_syntax.rTLabs_program -> state Errors.res
323 val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
326 'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
329 val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
331 val func_block_of_exec :
332 genv -> state -> Events.trace -> AST.ident ->
333 RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
334 Registers.register Types.option -> frame List.list -> GenMem.mem ->
335 Pointers.block Types.sig0