Library compcert.driver.Compopts

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.