diff options
Diffstat (limited to 'driver/Compopts.v')
| -rw-r--r-- | driver/Compopts.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/driver/Compopts.v b/driver/Compopts.v new file mode 100644 index 0000000..205f768 --- /dev/null +++ b/driver/Compopts.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Compilation options *) + +(** This file collects Coq functions to query the command-line + options that influence the code generated by the verified + part of CompCert. These functions are mapped by extraction + to accessors for the flags in [Clflags.ml]. *) + +(** Flag [-Os]. For instruction selection (mainly). *) +Parameter optim_for_size: unit -> bool. + +(** Flag [-ffloat-const-prop]. For value analysis and constant propagation. *) +Parameter propagate_float_constants: unit -> bool. +Parameter generate_float_constants: unit -> bool. + +(** For value analysis. Currently always false. *) +Parameter va_strict: unit -> bool. + +(** Flag -ftailcalls. For tail call optimization. *) +Parameter eliminate_tailcalls: unit -> bool. + + |