diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-16 11:10:28 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-16 11:10:28 +0200 |
| commit | 3344bcf59acb1ae8d43a0d15acb4b824689e706d (patch) | |
| tree | a5621a5d30ee7e39e2e6d2a95e02ab018e8ef846 /debug/Debug.mli | |
| parent | 36fe88d4cc2022947474a2fcc0b650e22f41ee3e (diff) | |
| download | compcert-kvx-3344bcf59acb1ae8d43a0d15acb4b824689e706d.tar.gz compcert-kvx-3344bcf59acb1ae8d43a0d15acb4b824689e706d.zip | |
Add the debug interface file.
The new file Debug.ml contains the interface for generating and
printing debug information. In order to generate debug information
the init function initializes the necessary functions depending
on the -g flag. If the -g is not there all functions are dummy
functions which do nothing.
Diffstat (limited to 'debug/Debug.mli')
| -rw-r--r-- | debug/Debug.mli | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/debug/Debug.mli b/debug/Debug.mli new file mode 100644 index 00000000..ea72aeb4 --- /dev/null +++ b/debug/Debug.mli @@ -0,0 +1,23 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open C +open Camlcoq + + +val init: unit -> unit +val init_compile_unit: string -> unit +val atom_function: ident -> atom -> unit +val atom_global_variable: ident -> atom -> unit +val set_composite_size: ident -> struct_or_union -> int -> unit +val set_member_offset: ident -> string -> int -> int -> unit +val insert_declaration: globdecl -> Env.t -> unit |