Module 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 optim_tailcalls: unit -> bool.

Flag -fconstprop. For constant propagation.
Parameter optim_constprop: unit -> bool.

Flag -fcse. For common subexpression elimination.
Parameter optim_CSE: unit -> bool.

Flag -fredundancy. For dead code elimination.
Parameter optim_redundancy: unit -> bool.

Flag -fthumb. For the ARM back-end.
Parameter thumb: unit -> bool.

Flag -g. For insertion of debugging information.
Parameter debug: unit -> bool.

Require Import BinNums DomKind Integers.

Flags -dom-z -dom-o -dom-p
Parameter num_dom: unit -> num_dom_kind.
Flag -max-concretize
Parameter max_concretize: unit -> N.
Flag -trace
Parameter trace: unit -> bool.
Flag -verbose
Parameter verbose: unit -> bool.
Flag -unroll n
Parameter unroll: unit -> nat.
Flag -size n
Parameter size: unit -> Integers.Int.int.
Generated by coq2html