From e7a5b00b7920ebf81591fc2f914483b6aa27269a Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Thu, 26 Jan 2017 10:07:48 +0100 Subject: describe environment variable for configuration file --- doc/ccomp.1 | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'doc/ccomp.1') 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 . -- cgit