blob: e2320418d044b4d8c3ef4a84a266ebde7f4b15ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open Asm
open AST
open BinNums
(** Auxiliary functions for builtin expansion *)
val emit: instruction -> unit
(* Emit an instruction *)
val new_label: unit -> label
(* Compute a fresh label *)
val is_current_function_variadic: unit -> bool
(* Test whether the current function is a variadic function *)
val get_current_function_args: unit -> typ list
(* Get the types of the current function arguments *)
val get_current_function_sig: unit -> signature
(* Get the signature of the current function *)
val set_current_function: coq_function -> unit
(* Set the current function *)
val get_current_function: unit -> coq_function
(* Get the current function *)
val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
(* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
function to get the dwarf mapping of variable names and for the expansion of simple instructions *)
|
