Add man page

2 files changed, 253 insertions, 0 deletions

diff --git a/debian/ccomp.1 b/debian/ccomp.1
new file mode 100644
index 0000000..8c35a66
--- /dev/null
+++ b/debian/ccomp.1
@@ -0,0 +1,252 @@
+.\"                                                                -*- nroff -*-
+.TH CCOMP "1" "February 5, 2015" "CompCert 2.4" "User Commands"
+.SH NAME
+ccomp \- CompCert C compiler
+.SH SYNOPSIS
+.B ccomp
+[\fIOPTION\fR]... \fISOURCE-FILE\fR...
+.SH DESCRIPTION
+
+CompCert, invoked as \fBccomp\fR, is a native-code compiler for a
+nearly-complete subset of C99 and a strict superset of MISRA-C 2004.  It
+produces code with performance characteristics comparable to that generated by
+\fBgcc(1)\fR at the \fB\-O1\fR optimization level.
+
+CompCert is unique among compilers in that it is written inside the Coq proof
+assistant, and its correctness has been formally verified.  That is, the Coq
+developers have mathematically proven that (modulo some minor assumptions) a
+program compiled with \fBccomp\fR will behave exactly as specified by the
+semantics of the original C source.
+
+.SH "RECOGNIZED SOURCE FORMATS"
+\fBccomp\fR recognizes source files with the following extensions.
+
+.TP
+\fB.c\fR
+C source code that must be preprocessed
+.TP
+\fB.i\fR, \fB.p\fR
+C source code that should not be preprocessed
+.TP
+\fB.cm\fR
+Cminor source code
+.TP
+\fB.s\fR
+assembler code
+.TP
+\fB.S\fR
+assembler code that must be preprocessed
+.TP
+\fB.o\fR
+object code
+.TP
+\fB.a\fR
+library archive
+
+.SH OPTIONS
+The following options modify \fBccomp\fR's behaviour.
+
+.SS "General options"
+.TP
+\fB\-stdlib\fR \fIdir\fR
+Set the path to CompCert's runtime library.
+.TP
+\fB\-v\fR
+Print each external command before invoking it.
+.TP
+\fB\-timings\fR
+Show the time spent in various compiler passes.
+
+.SS "Processing options"
+.TP
+\fB\-E\fR
+Stop execution after preprocessing and emit preprocessed code on standard output.
+.TP
+\fB\-S\fR
+Compile, but do not link; save generated assembly as a .s file.
+.TP
+\fB\-c\fR
+Compile, but do not link; save generated object code as a .o file.
+.TP
+\fB\-o\fR \fIfile\fR
+Save output as \fIfile\fR.
+
+.SS "Preprocessing options"
+.TP
+\fB\-I\fR\fIdir\fR
+Add \fIdir\fR to the preprocessor search path.
+.TP
+\fB\-D\fR\fIsymb\fR=\fIval\fR
+Define a preprocessor symbol.
+.TP
+\fB\-U\fR\fIsymb\fR
+Undefine a preprocessor symbol.
+.TP
+\fB\-Wp\fR,\fIopt\fR
+Pass option \fIopt\fR to the preprocessor.
+
+.SS "Language support options"
+Each of these options may be disabled by specifying \fB\-fno-\fIopt\fR.  For
+instance, specifying \fB\-fbitfields\fR forces struct bit field emulation;
+specifying \fB\-fno-bitfields\fR explicitly disables such emulation.
+
+.TP
+\fB\-fbitfields\fR
+Emulate bit fields in structs.  Disabled by default.
+.TP
+\fB\-flongdouble\fR
+Treat \fBlong double\fR as \fBdouble\fR.  Disabled by default.
+.TP
+\fB\-fstruct-return\fR
+Emulate returning structs and unions by value.  Disabled by default.
+.TP
+\fB\-fvararg-calls\fR
+Support calls to variable-argument functions.  Enabled by default.
+.TP
+\fB\-funprototyped\fR
+Support calls to old-style functions without prototypes.  Enabled by default.
+.TP
+\fB\-fpacked-structs\fR
+Emulate packed structs.  Disabled by default.
+.TP
+\fB\-finline-asm\fR
+Support inline assembly.  Disabled by default.
+.TP
+\fB\-fall\fR
+Enable all language support options.
+.TP
+\fB\-fnone\fR
+Disable all language support options.
+
+.SS "Debugging options"
+.TP
+\fB\-g\fR
+Place debugging information in generated code.
+
+.SS "Code generation options"
+Each binary option of the form \fB\-f\fIopt\fR may be disabled by specifying
+\fB\-fno-\fIopt\fR.  For instance, specifying \fB\-ftailcalls\fR enables
+tail-call optimization; \fB\-fno-tailcalls\fR explicitly disables such
+optimization.
+
+.TP
+\fB\-O\fR
+Optimize for speed.  This is the default.
+.TP
+\fB\-Os\fR
+Optimize for size.
+.TP
+\fB\-ffpu\fR
+Use floating-point registers for some integer operations.  Enabled by default.
+.TP
+\fB\-fsmall-data\fR \fIn\fR
+Set maximal size for allocation in the small data area to be \fIn\fR.
+.TP
+\fB\-fsmall-const\fR \fIn\fR
+Set maximal size for allocation in the small constant area to be \fIn\fR.
+.TP
+\fB\-ffloat-const-prop\fR \fIn\fR
+Control constant propagation of floating-point values.  With \fIn\fR set to 0,
+disable all float constant propagation; with \fIn\fR set to 2, enable all float
+constant propagation.  Setting \fIn\fR to 1 enables limited but not total
+constant propagation.  Default is 2.
+.TP
+\fB\-ftailcalls\fR
+Optimize function calls in tail position.  Enabled by default.
+.TP
+\fB\-falign-functions\fR \fIn\fR
+Ensure that function entry points are aligned to multiples of \fIn\fR bytes.
+.TP
+\fB\-falign-branch-targets\fR \fIn\fR
+Ensure that every branch target is aligned to a multiple of \fIn\fR bytes.
+.TP
+\fB\-falign-cond-branches\fR \fIn\fR
+Ensure that every conditional branch is aligned to a multiple of \fIn\fR bytes.
+
+.SS "Target processor options"
+.TP
+\fB\-mthumb\fR
+(ARM only) Use Thumb-2 instruction encoding.
+.TP
+\fB\-marm\fR
+(ARM only) Use ARM instruction encoding.
+
+.SS "Assembling options"
+.TP
+\fB\-Wa\fR,\fIopt\fR
+Pass option \fIopt\fR to the assembler.
+
+.SS "Linking options"
+.TP
+\fB\-l\fR\fIlib\fR
+Link against library \fIlib\fR.
+.TP
+\fB\-L\fR\fIdir\fR
+Add directory \fIdir\fR to the search path for libraries.
+.TP
+\fB\-Wl\fR,\fIopt\fR
+Pass option \fIopt\fR to the linker.
+
+.SS "Tracing options"
+.TP
+\fB\-dparse\fR
+Save C file after parsing and elaboration as \fIfile\fR.parse.c.
+.TP
+\fB\-dc\fR
+Save generated CompCert C as \fIfile\fR.compcert.c.
+.TP
+\fB\-dclight\fR
+Save generated Clight as \fIfile\fR.light.c.
+.TP
+\fB\-dcminor\fR
+Save generated Cminor as \fIfile\fR.cm.
+.TP
+\fB\-drtl\fR
+Save RTL at various optimization points as \fIfile\fR.rtl.\fIn\fR.
+.TP
+\fB\-dltl\fR
+Save LTL after register allocation as \fIfile\fR.ltl.
+.TP
+\fB\-dmach\fR
+Save generated Mach code as \fIfile\fR.mach.
+.TP
+\fB\-dasm\fR
+Save generated assembly as \fIfile\fR.s.
+.TP
+\fB\-sdump\fR
+Save information for post-linking validation as \fIfile\fR.sdump.
+
+.SS "Interpreter mode"
+.TP
+\fB\-interp\fR
+Execute the given C file using the reference interpreter.
+.TP
+\fB\-quiet\fR
+Suppress diagnostic messages from the interpreter.
+.TP
+\fB\-trace\fR
+Have the interpreter produce a detailed trace of reductions.
+.TP
+\fB\-random\fR
+Randomize execution order.
+.TP
+\fB\-all\fR
+Simulate all possible execution orders.
+
+.SH "SEE ALSO"
+\&\fIcoqc\fR\|(1), \fIgcc\fR\|(1)
+
+.SH AUTHOR
+CompCert is the work of many authors at the Institut National de Recherche en
+Informatique et en Automatique (INRIA).  Benjamin Barenblat wrote this manual
+page.
+
+.SH COPYRIGHT
+CompCert is copyright \(co 2004-2014 Institut National de Recherche en
+Informatique et en Automatique.  It is \fInot\fR free software: you can use it
+for evaluation, research, and education purposes, but not for commercial
+purposes.  See the INRIA Non-Commercial License Agreement
+<http://compcert.inria.fr/doc/LICENSE> for further details.
+
+This manual page is copyright \(co 2014, 2015 Benjamin Barenblat and licensed
+under the GNU GPL version 3 or later.
diff --git a/debian/compcert.manpages b/debian/compcert.manpages
new file mode 100644
index 0000000..fb9294b
--- /dev/null
+++ b/debian/compcert.manpages
@@ -0,0 +1 @@
+debian/ccomp.1
\ No newline at end of file