diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-01-26 10:07:48 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2017-01-26 10:07:48 +0100 |
| commit | e7a5b00b7920ebf81591fc2f914483b6aa27269a (patch) | |
| tree | 518dc8a7844f4c0f9ec27ca615149aeb6711cc3e /doc/ccomp.1 | |
| parent | c2f22b1314148b79bb92a1ef116c1b732fcc5e34 (diff) | |
| download | compcert-kvx-e7a5b00b7920ebf81591fc2f914483b6aa27269a.tar.gz compcert-kvx-e7a5b00b7920ebf81591fc2f914483b6aa27269a.zip | |
describe environment variable for configuration file
Diffstat (limited to 'doc/ccomp.1')
| -rw-r--r-- | doc/ccomp.1 | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/doc/ccomp.1 b/doc/ccomp.1 index c02d3571..1aea4ff1 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 @@ -537,5 +536,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>. |