aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-0/+2
|\
| * Added flag to desactivate condition inversionCyril SIX2020-02-031-0/+1
| |
| * Tail duplication optimization defaulting to offCyril SIX2020-01-271-1/+1
| |
| * Added a flag to desactivate tail duplicationCyril SIX2020-01-271-0/+1
| |
* | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-0/+1
|\ \ | |/ |/|
| * connected (just a silly problem)David Monniaux2020-01-281-0/+1
| |
* | connect forward-moves to compilerDavid Monniaux2020-01-081-1/+2
| |
* | -fall-loads-nontrapDavid Monniaux2019-09-091-0/+1
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-1/+1
|\| | | | | | | mppa-work-upstream-merge
| * Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-1/+1
| | | | | | | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
| * If-conversion optimizationXavier Leroy2019-06-061-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-0/+3
|\ \ | | | | | | | | | mppa-if-conversion
| * | If-conversion optimizationXavier Leroy2019-05-311-0/+2
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+1
| | | | | | | | | | | | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
* | option -faddx (off by default until questions cleared)David Monniaux2019-05-111-1/+2
| |
* | -fcoalesce-memDavid Monniaux2019-05-031-0/+1
| |
* | Merge branch 'mppa-xsaddr' into mppa-workDavid Monniaux2019-05-021-0/+4
|\ \
| * | command line options (still incomplete)David Monniaux2019-05-021-0/+4
| | |
* | | The scheduler selection works, but the argument is not optional yet ↵Cyril SIX2019-04-291-1/+1
|/ / | | | | | | (-fpostpass nameofscheduler)
* | -fpostpass-ilpDavid Monniaux2019-03-121-0/+1
| |
* | Added long double = double by default on Kalray architectureCyril SIX2019-03-011-1/+1
| |
* | -O0 will not perform postpass schedulingCyril SIX2019-01-181-0/+1
|/
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-071-0/+1
| | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated.
* Add optimization option finline.Bernhard Schommer2017-04-071-0/+1
| | | | | | The new option f(no-)inline controlls whether inlining is active or not. Bug 21343.
* Refactored debugging options.Bernhard Schommer2016-10-141-1/+1
| | | | | | | The options controlling the generation of debugging information are now moved into the Debug module. Futhermore the -gdepth options are replaced in favor of a more gcc compatible version. Bug 20193
* Remove undocumented option. Bug 20193Bernhard Schommer2016-10-141-1/+0
|
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-0/+2
| | | | | | | Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
* Added option to dump preprocessed source code.Bernhard Schommer2016-01-221-0/+1
| | | | The new option -dprepro allows it to keep the preprocessed source code files.
* Revise and simplify the -fstruct-return and -fstruct-passing options.Xavier Leroy2015-12-081-3/+1
| | | | | | - Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing' - Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful. - Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
* Added now option to control debug output.Bernhard Schommer2015-11-161-1/+1
| | | | | | | | | | | The new option gdepth subumes the gonly-globals. The option allows it to control the level of information that is produced. This option allows it to generate debugging inforation for: -Only globals -Global and local variables but without location information for the local variable -Full information Bug 17638.
* New option to control the debug information build.Bernhard Schommer2015-11-041-0/+1
| | | | | | The new option -gonly-global allows the generation of debuging information for global variables only. Bug 17566.
* Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-161-0/+1
| | | | | | | | | | The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392.
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-1/+1
|
* Added flag for the renaming of static functions.Bernhard Schommer2015-05-191-0/+1
|
* Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-2/+2
| | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
* Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-141-0/+2
| | | | | | | | configure: special ABI value for IA32/MacOSX and PowerPC/Linux cparser/Machine: special config for PowerPC/Linux cparser/StructReturn: generate better code for return-as-int driver/Clflags, driver/Driver: add options -fstruct-return=<convention> and -fstruct-passing=<convention> to simplify testing
* Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-161-0/+3
| | | | them off.
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-50/+0
|
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-191-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* configure: distinguish between ABI and processor model.xleroy2014-07-291-2/+2
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-061-0/+51
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-0/+1
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-6/+1
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More tolerance for functions declared without a prototypexleroy2013-12-281-0/+1
| | | | | | | | (option -funprototyped, on by default). Error if call to vararg function and -fvararg-calls is off. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2389 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-0/+1
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-201-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename "-fno-sse" into "-fno-fpu" and honor it on PowerPC as well.xleroy2013-11-271-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2374 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem ↵xleroy2013-05-171-0/+1
| | | | | | | | | with some static analysis tools). */PrintAsm.ml: don't cfa_adjust at Pfreeframe, as more code from the function can appear after (in case of tailcalls). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2256 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for debugging info (-g).xleroy2013-05-171-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-11 23:30:26 +0000