aboutsummaryrefslogtreecommitdiffstats
path: root/backend/JsonAST.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2018-01-05 09:50:10 +0100
committerGitHub <noreply@github.com>2018-01-05 09:50:10 +0100
commit9ccb6a24541b3a06b600a70791950eecd46d1806 (patch)
tree4b7389a1085bb4e744a129dd97f4d03dafb5ea7e /backend/JsonAST.mli
parent8219490aae44fa79932d913cc69941d6b22a70a3 (diff)
downloadcompcert-kvx-9ccb6a24541b3a06b600a70791950eecd46d1806.tar.gz
compcert-kvx-9ccb6a24541b3a06b600a70791950eecd46d1806.zip
Resynchronize the LICENSE file and the license headers in individual files (#45)
Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
Diffstat (limited to 'backend/JsonAST.mli')
-rw-r--r--backend/JsonAST.mli16
1 files changed, 16 insertions, 0 deletions
diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli
new file mode 100644
index 00000000..c6fd80c9
--- /dev/null
+++ b/backend/JsonAST.mli
@@ -0,0 +1,16 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+
+
+val pp_program : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
+val pp_mnemonics : Format.formatter -> string list -> unit