diff options
Diffstat (limited to 'doc/ccomp.1')
| -rw-r--r-- | doc/ccomp.1 | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/doc/ccomp.1 b/doc/ccomp.1 index ef4d7743..d84adc7f 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -16,8 +16,7 @@ In other words, the executable code it produces is proved to behave exactly as s 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 +.SH RECOGNIZED SOURCE FILES . .TP .B .c @@ -48,6 +47,18 @@ Object file. Library file. . .SH OPTIONS +.SS General Options +.INDENT 0.0 +. +.TP +.B \-conf <file> +Read CompCert configuration from <file>. This takes precedence over any other specification. +. +.TP +.B \-target <triple> +Read CompCert configuration from <triple>.ini instead of using the default of compcert.ini. +The configuration file is searched for in the share directory of the CompCert installation. +. .SS Processing Options .INDENT 0.0 . @@ -219,7 +230,7 @@ Debugging Options . .TP .B \-g -Generate debugging information. +Generate full debugging information. . .TP .BR \-g0 ", " \-g1 ", " \-g2 ", " \-g3 @@ -537,5 +548,14 @@ Randomize execution order. .TP .B \-all Simulate all possible execution orders. +. +.SH ENVIRONMENT +. +.TP +.B COMPCERT_CONFIG +If this environment variable is present, it denotes the path to the CompCert configuration file to be used. +The variable takes precedence over default search paths or the \fB\-target\fP option, but has a lower priority than the \fB\-conf\fP option. +. .SH BUGS +. To report bugs, please visit <https://github.com/AbsInt/CompCert/issues>. |