diff options
| -rw-r--r-- | debian/ccomp.1 | 252 | ||||
| -rw-r--r-- | debian/compcert.manpages | 1 |
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 |