From 20ee821830467d091984ccf9ed646de7975866a7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 5 Feb 2015 13:02:29 +0100 Subject: Changed the ASM printer of the powerpc to the generalized backend. --- backend/PrintAsm.mli | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 backend/PrintAsm.mli (limited to 'backend/PrintAsm.mli') diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli new file mode 100644 index 00000000..eb63f1be --- /dev/null +++ b/backend/PrintAsm.mli @@ -0,0 +1,16 @@ +(* *********************************************************************) +(* *) +(* 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 PrintAsmaux + +val print_program: out_channel -> Asm.program -> unit -- cgit