From d88a7116afa51df41ba3495c9891959830497452 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Fri, 14 Oct 2016 14:18:43 +0200 Subject: Add a man-page --- doc/ccomp.1 | 534 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 534 insertions(+) create mode 100644 doc/ccomp.1 (limited to 'doc/ccomp.1') diff --git a/doc/ccomp.1 b/doc/ccomp.1 new file mode 100644 index 00000000..78da8191 --- /dev/null +++ b/doc/ccomp.1 @@ -0,0 +1,534 @@ +.TH CCOMP 1 +.SH NAME +ccomp \- the CompCert C compiler +. +.SH SYNOPSIS +\fBccomp\fP [\fIoptions\fP] \fIfile ...\fP +. +.SH DESCRIPTION +\fBCompCert C\fP is a compiler for the C programming language. +Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance. +It accepts most of the ISO C 99 language, with some exceptions and a few extensions. +It produces machine code for the PowerPC, ARM, and IA32 (x86 32-bits) architectures. +.PP +What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. +In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program. +This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance. +In particular, using the CompCert C compiler is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source code level: the correctness proof of CompCert C guarantees that all safety properties verified on the source code automatically hold as well for the generated executable. +. +.SH +RECOGNIZED SOURCE FILES +. +.TP +.B .c +C source file. +. +.TP +.BR .i ", " .p +C source file that should not be preprocessed. +. +.TP +.B .cm +Cminor source file. +. +.TP +.B .s +Assembly file. +. +.TP +.B .S +Assembly file that must be preprocessed. +. +.TP +.B .o +Object file. +. +.TP +.B .a +Library file. +. +.SH OPTIONS +.SS Processing Options +.INDENT 0.0 +. +.TP +.B \-c +Compile to object file only (no linking), result in .o. +. +.TP +.B \-E +Preprocess only, send result to standard output. +. +.TP +.B \-S +Compile to assembler only, save result in .s. +. +.TP +.B \-o +Generate output to . +. +.SS Preprocessing Options +.INDENT 0.0 +. +.TP +.B \-I +Add to search path for include files. +. +.TP +.B \-include +Process as if \fB#include ""\fP appears at the first line of the primary source file. +. +.TP +.B \-D= +Define a preprocessor symbol. +. +.TP +.B \-U +Undefine a preprocessor symbol. +. +.TP +.B \-Wp, +Pass comma separated arguments in to the preprocessor. +. +.TP +.B \-Xpreprocessor +Pass argument to the preprocessor. +. +.TP +.BR \-C ", " \-CC ", " \-idirafter ", " \-imacros ", " \-iquote ", " \-isystem ", " \-M ", " \-MF ", " \-MG ", " \-MM ", " \-MP ", " \-MQ ", " \-MT ", " \-nostdinc ", " \-P +For GNU backends these options are recognized by CompCert and passed through to the preprocessor. +. +.SS +Optimization Options +.INDENT 0.0 +. +.TP +.B \-O +Optimize the compiled code. +Enabled by default. +. +.TP +.B \-O0 +Turn off most optimizations. +Synonymous to \fB\-fno\-const\-prop\fP \fB\-fno\-cse\fP \fB\-fno\-redundancy\fP \fB\-fno\-tailcalls\fP. +. +.TP +.BR \-O1 ", " \-O2 ", " \-O3 +Synonymous for \fB\-O\fP. +. +.TP +.B \-Os +Optimize for code size in preference to code speed. +. +.TP +.BR \-fconst\-prop ", " \-fno\-const\-prop +Turn on/off global constant propagation. +Enabled by default. +. +.TP +.BR \-fcse ", " \-fno\-cse +Turn on/off common subexpression elimination. +Enabled by default. +. +.TP +.BR \-fredundancy ", " \-fno\-redundancy +Turn on/off redundancy elimination. +Enabled by default. +. +.TP +.BR \-ftailcalls ", " \-fno\-tailcalls +Turn on/off optimization of function calls in tail position. +Enabled by default. +. +.TP +.B \-ffloat\-const\-prop +Control constant propagation of floats (=0: none, =1: limited, =2: full). +Default is full. +. +.SS +Code Generation Options +.INDENT 0.0 +. +.TP +.B \-falign\-functions +Set alignment of function entry points to bytes. +The default alignment is 16 bytes for IA-32 targets and 4 bytes for ARM and PowerPC. +. +.TP +.BR \-ffpu ", " \-fno\-fpu +Turn on/off use of FP registers for some integer operations. +Enabled by default. +. +.SS +Code Generation Options (PowerPC with Diab Backend) +.INDENT 0.0 +. +.TP +.B \-falign\-branch\-targets +Set alignment of branch targets to bytes. +The default alignment is 0 bytes which deactivates alignment of branch targets. +. +.TP +.B \-falign\-cond\-branches +Set alignment of conditional branches to bytes. +The default alignment is 0 bytes which deactivates alignment of conditional branch targets. +. +.TP +.B \-fsmall\-const +Set maximal size for allocation in small data constant to bytes. +The default is 8 bytes. +. +.TP +.B \-fsmall\-data +Set maximal size for allocation in small data area to bytes. +The default is 8 bytes. +. +.SS +Code Generation Options (ARM Targets) +.INDENT 0.0 +. +.TP +.B \-mthumb +Generate code using the Thumb 2 instruction encoding. +This is the default if CompCert is configured for the ARMv7R profile. +. +.TP +.B \-marm +Generate code using the ARM instruction encoding. +This is the default if CompCert is configured for a profile other than ARMv7R. +. +.SS +Assembling Options +.INDENT 0.0 +. +.TP +.B \-Wa, +Pass comma separated arguments in to the assembler. +. +.TP +.B \-Xassembler +Pass argument to the assembler. +. +.SS +Debugging Options +.INDENT 0.0 +. +.TP +.B \-g +Generate debugging information. +. +.TP +.B \-gdepth +Control generation of debugging information (=0: none, =1: only-globals, =2: globals and locals without locations, =3: full). +The default level is 3 for full debugging information. +. +.SS +Debugging Options (GNU Backend) +.INDENT 0.0 +. +.TP +.B \-gdwarf- +For GNU backends select debug information in DWARF format version 2 or 3. +The default format is DWARF v2. +. +.SS +Linking Options +.INDENT 0.0 +. +.TP +.B \-l +Link library . +. +.TP +.B \-L +Add to search path for libraries. +. +.TP +.B \-Wl, +Pass comma separated arguments in to the linker. +. +.TP +.B \-WUl, +Pass comma separated arguments in to the driver program used for linking. +. +.TP +.B \-Xlinker +Pass argument to the linker. +. +.TP +.B \-s +Remove all symbol table and relocation information from the executable. +. +.TP +.B \-static +Prevent linking with the shared libraries. +. +.TP +.B \-T +Use as linker command file. +. +.TP +.B \-u +Pretend the symbol is undefined to force linking of library modules to define it. +. +.TP +.BR \-nodefaultlibs ", " \-nostartfiles ", " \-nostdlib +For GNU backends these options are recognized by CompCert and passed through to the linker. +. +.SS +Language Support Options +.INDENT 0.0 +. +.TP +.BR \-fbitfields ", " \-fno\-bitfields +Turn on/off support for emulation bit fields in structs. +Disabled by default. +. +.TP +.BR \-flongdouble ", " \-fno\-longdouble +Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP. +Disabled by default. +. +.TP +.BR \-fpacked\-structs ", " \-fno\-packed\-structs +Turn on/off support for emulation of packed structs. +Disabled by default. +. +.TP +.BR \-fstruct\-passing ", " \-fno\-struct\-passing\fR +Turn on/off support for passing structs and unions by value as function results or function arguments. +Disabled by default. +. +.TP +.BR \-funprototyped ", " \-fno\-unprototyped +Turn on/off support calls to old-style functions without prototypes. +Enabled by default. +. +.TP +.BR \-fvararg\-calls ", " \-fno\-vararg\-calls +Turn on/off support for calls to variable-argument functions. +Enabled by default. +. +.TP +.BR \-finline-asm ", " \-fno\-inline-asm +Turn on/off support for inline \fBasm\fP statements. +Disabled by default. +. +.TP +.B \-fall +Activate all language support options above. +. +.TP +.B \-fnone +Deactivate all language support options above. +. +.SS +Diagnostic Options +.INDENT 0.0 +. +.TP +.B \-Wall +Enable all warnings. +. +.TP +.B \-W +Enable the specific warning . +CompCert supports the following warning classes: +.sp +\fIc11\-extensions\fP: +Feature specific to C11. +Enabled by default. +.sp +\fIcompare\-distinct\-pointer\-types\fP: +Comparison of different pointer types. +Enabled by default. +.sp +\fIcompcert\-conformance\fP: +Features that are not part of the CompCert C core language, e.g. K&R style functions. +Disabled by default. +.sp +\fIconstant\-conversion\fP: +Dangerous conversion of constants, e.g. literals that are too large for the given type. +Enabled by default. +.sp +\fIgnu\-empty\-struct\fP: +GNU extension for empty structs. +Enabled by default. +.sp +\fIimplicit\-function\-declaration\fP: +Deprecated implicit function declarations. +Enabled by default. +.sp +\fIimplicit\-int\fP: +Type of parameter or return type is implicitly assumed to be int. +Enabled by default. +.sp +\fIint\-conversion\fP: +Conversion between pointer and integer. +Enabled by default. +.sp +\fIinvalid\-noreturn\fP: +Functions declared as noreturn that actually contain a return statement. +Enabled by default. +.sp +\fIliteral\-range\fP: +Floating point literals with out-of-range magnitudes or values that convert to NaN. +Enabled by default. +.sp +\fImain\-return\-type\fP: +Wrong return type for main. +Enabled by default. +.sp +\fIpointer\-type\-mismatch\fP: +Use of incompatible pointer types in conditional expressions. +Enabled by default. +.sp +\fIreturn\-type\fP: +Void-return statement in non-void function. +Enabled by default. +.sp +\fIunknown\-attributes\fP: +Use of unsupported or unknown attributes. +Enabled by default. +.sp +\fIunknown\-pragmas\fP: +Use of unsupported or unknown pragmas. +Disabled by default. +.sp +\fIvarargs\fP: +Promotable vararg arguments. +Enabled by default. +.sp +\fIzero\-length\-array\fP: +GNU extension for zero length arrays. +Disabled by default. +. +.TP +.B \-Wno- +Disable the specific warning . +. +.TP +.B \-Werror +Treat all warnings of CompCert as errors. +. +.TP +.B \-Werror= +Treat the specific warning as an error. +. +.TP +.B \-Wno-error= +Prevent the specific warning from being treated as error even if \fB\-Werror\fP is specified. +. +.TP +.B \-Wfatal-errors +Treat all errors of CompCert as fatal errors, so that the compilation is aborted immediately. +. +.TP +.B \-fdiagnostics-color +Turn on colored diagnostics. Default for TTY output devices. +. +.TP +.B \-fno-diagnostics-color +Turn of colored diagnostics. +. +.SS +Tracing Options +.INDENT 0.0 +. +.TP +.B \-dprepro +Save C file after preprocessing in .i +. +.TP +.B \-dparse +Save C file after parsing and elaboration in .parsed.c. +. +.TP +.B \-dc +Save generated CompCert C in .compcert.c. +. +.TP +.B \-dclight +Save generated Clight in .light.c. +. +.TP +.B \-dcminor +Save generated Cminor in .cm. +. +.TP +.B \-drtl +Save RTL at various optimization points in .rtl.. +. +.TP +.B \-dltl +Save LTL after register allocation in .ltl. +. +.TP +.B \-dmach +Save generated Mach code in .mach. +. +.TP +.B \-dasm +Save generated assembly in .s. +. +.TP +.B \-dall +Save all generated intermediate files in .. +. +.TP +.B \-doptions +Save the compiler configuration in .opt.json. +. +.TP +.B \-sdump +Save abstract syntax tree of generated assembly for post-linking validation tool in .json. +. +.SS +Miscellaneous Options +.INDENT 0.0 +. +.TP +.B \-stdlib +Set the path of the CompCert run-time library to . +. +.TP +.B \-v +Print external commands before invoking them. +. +.TP +.B \-timings +Print information about the time spent in various compiler passes. +. +.TP +.B \-version +Print the CompCert version information and exit. +. +.TP +.B @ +Read command line options from . +. +.SS +Interpreter Mode +.INDENT 0.0 +. +.TP +.B \-interp +Execute the given .c files using the reference interpreter. +. +.TP +.B \-quiet +Suppress diagnostic messages for the interpreter. +. +.TP +.B \-trace +Have the interpreter produce a detailed trace of reductions. +. +.TP +.B \-random +Randomize execution order. +. +.TP +.B \-all +Simulate all possible execution orders. +.SH BUGS +To report bugs, please visit . -- cgit