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 -fcse2. For DMonniaux's common subexpression elimination.
Parameter optim_CSE2: unit -> bool.

Flag -fcse3. For DMonniaux's common subexpression elimination.
Parameter optim_CSE3: unit -> bool.

Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. Perform a simple alias analysis.
Parameter optim_CSE3_alias_analysis: unit -> bool.

Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across function calls (may increase register pressure).
Parameter optim_CSE3_across_calls: unit -> bool.

Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across control-flow merges (may increase register pressure).
Parameter optim_CSE3_across_merges: unit -> bool.

Flag -fcse3-glb
Parameter optim_CSE3_glb: unit -> bool.

Flag -fcse3-trivial-ops. For DMonniaux's common subexpression elimination, simplify trivial operations as well.
Parameter optim_CSE3_trivial_ops: unit -> bool.

Flag -fcse3-conditions. For DMonniaux's common subexpression elimination: remove redundant conditional branches.
Parameter optim_CSE3_conditions: unit -> bool.

Flag -fmove-loop-invariants.
Parameter optim_move_loop_invariants: unit -> bool.

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

Flag -fpostpass. Postpass scheduling for K1 architecture
Parameter optim_postpass: unit -> bool.

FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false)
Parameter optim_globaladdrtmp: unit -> bool.

FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false)
Parameter optim_globaladdroffset: unit -> bool.

FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true)
Parameter optim_xsaddr: unit -> bool.

Flag -fcoaelesce-mem. Fuse (default true)
Parameter optim_coalesce_mem: unit -> bool.

Parameter optim_madd: unit -> bool.

FIXME TEMPORARY Flag -faddx. Fuse (default false)
Parameter optim_addx: unit -> bool.

Parameter optim_leaf: unit -> bool.

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

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

Flag -fall-loads-nontrap. Turn user loads into non trapping.
Parameter all_loads_nontrap: unit -> bool.

Flag -fforward-moves. Forward moves after CSE.
Parameter optim_forward_moves: unit -> bool.

Flag -fprofile-arcs. Add profiling logger.
Parameter profile_arcs : unit -> bool.

Flag -fbranch_probabilities. Use profiling information if available
Parameter branch_probabilities : unit -> bool.

Flag -fbranch-target-protection.
Parameter branch_target_protection : unit -> bool.

Flag -freturn-address-protection .
Parameter return_address_protection : unit -> bool.

Flag -faarch64-has-pac .
Parameter aarch64_has_pac : unit -> bool.

fexpanse-rtlcond \/ fexpanse-others
Parameter optims_expanse : unit -> bool.

Parameter optim_lct : unit -> bool.

Parameter btl_bb : unit -> bool.

Parameter btl_sb : unit -> bool.

Parameter lct_tun : unit -> bool.

Generate inline division
Parameter inline_fp_div32 : unit -> bool.
Parameter inline_fp_div64 : unit -> bool.

Require Import Coqlib.
Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
Generated by coq2html