107 open Hints_declaration
119 open RTLabs_semantics
121 type rTLabs_state = RTLabs_semantics.state
123 type rTLabs_genv = RTLabs_semantics.genv
129 open StructuredTraces
135 val status_class_jmdiscr :
136 StructuredTraces.status_class -> StructuredTraces.status_class -> __
138 type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
139 ras_fn_stack : Pointers.block List.list }
141 val rTLabs_ext_state_rect_Type4 :
142 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
143 List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
145 val rTLabs_ext_state_rect_Type5 :
146 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
147 List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
149 val rTLabs_ext_state_rect_Type3 :
150 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
151 List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
153 val rTLabs_ext_state_rect_Type2 :
154 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
155 List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
157 val rTLabs_ext_state_rect_Type1 :
158 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
159 List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
161 val rTLabs_ext_state_rect_Type0 :
162 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
163 List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
166 RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
169 RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list
171 val rTLabs_ext_state_inv_rect_Type4 :
172 RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
173 Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
175 val rTLabs_ext_state_inv_rect_Type3 :
176 RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
177 Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
179 val rTLabs_ext_state_inv_rect_Type2 :
180 RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
181 Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
183 val rTLabs_ext_state_inv_rect_Type1 :
184 RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
185 Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
187 val rTLabs_ext_state_inv_rect_Type0 :
188 RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
189 Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
191 val rTLabs_ext_state_discr :
192 RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __
194 val rTLabs_ext_state_jmdiscr :
195 RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __
197 val dpi1__o__Ras_state__o__inject :
198 RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
199 RTLabs_semantics.state Types.sig0
201 val eject__o__Ras_state__o__inject :
202 RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
203 RTLabs_semantics.state Types.sig0
205 val ras_state__o__inject :
206 RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
209 val dpi1__o__Ras_state :
210 RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
211 RTLabs_semantics.state
213 val eject__o__Ras_state :
214 RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
215 RTLabs_semantics.state
218 RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
219 Events.trace -> rTLabs_ext_state
221 val rTLabs_classify : RTLabs_semantics.state -> StructuredTraces.status_class
223 val rTLabs_cost : RTLabs_semantics.state -> Bool.bool
225 val rTLabs_cost_label :
226 RTLabs_semantics.state -> CostLabel.costlabel Types.option
229 | Rapc_state of Pointers.block * Graphs.label
230 | Rapc_call of Graphs.label Types.option * Pointers.block
231 | Rapc_ret of Pointers.block Types.option
234 val rTLabs_pc_rect_Type4 :
235 (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
236 Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
239 val rTLabs_pc_rect_Type5 :
240 (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
241 Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
244 val rTLabs_pc_rect_Type3 :
245 (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
246 Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
249 val rTLabs_pc_rect_Type2 :
250 (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
251 Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
254 val rTLabs_pc_rect_Type1 :
255 (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
256 Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
259 val rTLabs_pc_rect_Type0 :
260 (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
261 Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
264 val rTLabs_pc_inv_rect_Type4 :
265 rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
266 Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
267 Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
269 val rTLabs_pc_inv_rect_Type3 :
270 rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
271 Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
272 Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
274 val rTLabs_pc_inv_rect_Type2 :
275 rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
276 Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
277 Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
279 val rTLabs_pc_inv_rect_Type1 :
280 rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
281 Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
282 Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
284 val rTLabs_pc_inv_rect_Type0 :
285 rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) -> (Graphs.label
286 Types.option -> Pointers.block -> __ -> 'a1) -> (Pointers.block
287 Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
289 val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __
291 val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __
293 val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool
295 val rTLabs_deqset : Deqsets.deqSet
297 val rTLabs_ext_state_to_pc : RTLabs_semantics.genv -> rTLabs_ext_state -> __
299 val rTLabs_pc_to_cost_label :
300 RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
301 -> CostLabel.costlabel Types.option
303 val rTLabs_call_ident :
304 RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident
306 val rTLabs_status : RTLabs_semantics.genv -> StructuredTraces.abstract_status
308 val eval_ext_statement :
309 RTLabs_semantics.genv -> rTLabs_ext_state -> (IO.io_out, IO.io_in,
310 (Events.trace, rTLabs_ext_state) Types.prod) IOMonad.iO
312 val rTLabs_ext_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
314 val make_ext_initial_state :
315 RTLabs_syntax.rTLabs_program -> rTLabs_ext_state Errors.res
317 val rTLabs_ext_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec