133 open Hints_declaration
153 type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
154 stackp : ByteValues.xpointer }
156 val reg_sp_rect_Type4 :
157 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
160 val reg_sp_rect_Type5 :
161 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
164 val reg_sp_rect_Type3 :
165 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
168 val reg_sp_rect_Type2 :
169 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
172 val reg_sp_rect_Type1 :
173 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
176 val reg_sp_rect_Type0 :
177 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
180 val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map
182 val stackp : reg_sp -> ByteValues.xpointer
184 val reg_sp_inv_rect_Type4 :
185 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
186 ByteValues.xpointer -> __ -> 'a1) -> 'a1
188 val reg_sp_inv_rect_Type3 :
189 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
190 ByteValues.xpointer -> __ -> 'a1) -> 'a1
192 val reg_sp_inv_rect_Type2 :
193 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
194 ByteValues.xpointer -> __ -> 'a1) -> 'a1
196 val reg_sp_inv_rect_Type1 :
197 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
198 ByteValues.xpointer -> __ -> 'a1) -> 'a1
200 val reg_sp_inv_rect_Type0 :
201 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
202 ByteValues.xpointer -> __ -> 'a1) -> 'a1
204 val reg_sp_discr : reg_sp -> reg_sp -> __
206 val reg_sp_jmdiscr : reg_sp -> reg_sp -> __
208 val dpi1__o__reg_sp_env__o__inject :
209 (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
212 val eject__o__reg_sp_env__o__inject :
213 reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0
215 val reg_sp_env__o__inject :
216 reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0
218 val dpi1__o__reg_sp_env :
219 (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
221 val eject__o__reg_sp_env :
222 reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
225 PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
227 val reg_sp_retrieve :
228 reg_sp -> Registers.register -> ByteValues.beval Errors.res
230 val reg_sp_empty : ByteValues.xpointer -> reg_sp
232 type frame = { fr_ret_regs : Registers.register List.list;
233 fr_pc : ByteValues.program_counter;
234 fr_carry : ByteValues.bebit; fr_regs : reg_sp }
236 val frame_rect_Type4 :
237 (Registers.register List.list -> ByteValues.program_counter ->
238 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
240 val frame_rect_Type5 :
241 (Registers.register List.list -> ByteValues.program_counter ->
242 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
244 val frame_rect_Type3 :
245 (Registers.register List.list -> ByteValues.program_counter ->
246 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
248 val frame_rect_Type2 :
249 (Registers.register List.list -> ByteValues.program_counter ->
250 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
252 val frame_rect_Type1 :
253 (Registers.register List.list -> ByteValues.program_counter ->
254 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
256 val frame_rect_Type0 :
257 (Registers.register List.list -> ByteValues.program_counter ->
258 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
260 val fr_ret_regs : frame -> Registers.register List.list
262 val fr_pc : frame -> ByteValues.program_counter
264 val fr_carry : frame -> ByteValues.bebit
266 val fr_regs : frame -> reg_sp
268 val frame_inv_rect_Type4 :
269 frame -> (Registers.register List.list -> ByteValues.program_counter ->
270 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
272 val frame_inv_rect_Type3 :
273 frame -> (Registers.register List.list -> ByteValues.program_counter ->
274 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
276 val frame_inv_rect_Type2 :
277 frame -> (Registers.register List.list -> ByteValues.program_counter ->
278 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
280 val frame_inv_rect_Type1 :
281 frame -> (Registers.register List.list -> ByteValues.program_counter ->
282 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
284 val frame_inv_rect_Type0 :
285 frame -> (Registers.register List.list -> ByteValues.program_counter ->
286 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
288 val frame_discr : frame -> frame -> __
290 val frame_jmdiscr : frame -> frame -> __
292 val rTL_state_params : Joint_semantics.sem_state_params
294 type rTL_state = Joint_semantics.state
296 val rtl_arg_retrieve :
297 reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res
300 rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod Errors.res
302 val rtl_init_local : Registers.register -> reg_sp -> reg_sp
304 val rtl_setup_call_separate :
305 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
306 rTL_state -> rTL_state Errors.res
308 val rtl_setup_call_separate_overflow :
309 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
310 rTL_state -> rTL_state Errors.res
312 val rtl_setup_call_unique :
313 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
314 rTL_state -> rTL_state Errors.res
316 type rTL_state_pc = Joint_semantics.state_pc
318 val rtl_save_frame : Registers.register List.list -> rTL_state_pc -> __
320 val rtl_fetch_external_args :
321 AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
322 Values.val0 List.list Errors.res
325 Values.val0 List.list -> Registers.register List.list -> rTL_state ->
329 PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
330 Joint_semantics.state
332 val rtl_reg_retrieve :
333 Joint_semantics.state -> Registers.register -> ByteValues.beval Errors.res
335 val rtl_read_result :
336 Registers.register List.list -> rTL_state -> ByteValues.beval List.list
339 val rtl_pop_frame_separate :
340 Registers.register List.list -> rTL_state -> (rTL_state,
341 ByteValues.program_counter) Types.prod Errors.res
343 val rtl_pop_frame_unique :
344 Registers.register List.list -> rTL_state -> (rTL_state,
345 ByteValues.program_counter) Types.prod Errors.res
347 val block_of_register_pair :
348 Registers.register -> Registers.register -> rTL_state -> Pointers.block
352 RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res
355 PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
358 val rTL_semantics_separate : SemanticsUtils.sem_graph_params
360 val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params
362 val rTL_semantics_unique : SemanticsUtils.sem_graph_params