diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-16 11:06:54 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-16 11:06:54 +0100 |
| commit | 7035f06bf453bdf2f9f09fd8a392778e9ad3cd43 (patch) | |
| tree | 529e55a00a8882c5f9d7e701be125379e0d15efb /arm/AsmToJSON.mli | |
| parent | c54e20b2c444ddbb561bb4ac0422c92b77b656b1 (diff) | |
| download | compcert-kvx-7035f06bf453bdf2f9f09fd8a392778e9ad3cd43.tar.gz compcert-kvx-7035f06bf453bdf2f9f09fd8a392778e9ad3cd43.zip | |
Cleanup of AsmToJSON.
Removed unused code, factored out common functions and added an
interface file.
Bug 18394
Diffstat (limited to 'arm/AsmToJSON.mli')
| -rw-r--r-- | arm/AsmToJSON.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli new file mode 100644 index 00000000..20bcba5e --- /dev/null +++ b/arm/AsmToJSON.mli @@ -0,0 +1,13 @@ +(* *********************************************************************) +(* *) +(* 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 p_program: out_channel -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit |