aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Allow the option -o to be also the prefix of the file name for compability ↵Bernhard Schommer2015-05-311-0/+2
| |/ | | | | | | with different build systems.
* | Added flag for the renaming of static functions.Bernhard Schommer2015-05-191-0/+2
| |
* | Moved the information needed from the atoms to the ASM printer and removed ↵Bernhard Schommer2015-05-061-2/+2
| | | | | | | | unused information from the json dump.
* | Added the first version of the sdump export to json.Bernhard Schommer2015-04-271-2/+14
|/
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-2/+30
|\ | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-11/+12
| | | | | | | | | | | | | | | | 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.
| * Merge branch 'master' into struct-passingXavier Leroy2015-03-141-32/+56
| |\
| * | Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-141-3/+27
| | | | | | | | | | | | | | | | | | | | | | | | 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
| * | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-271-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* | | Added missing functions for printing the structs and unions. Still missing ↵Bernhard Schommer2015-03-241-8/+4
| | | | | | | | | | | | printing of packed structs.
* | | Activating the printing of the debug information for supported architecture.Bernhard Schommer2015-03-191-6/+10
| | |
* | | Added function to convert C types into their dwarf represnation.Bernhard Schommer2015-03-181-2/+3
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2015-03-101-32/+56
|\ \ \ | | |/ | |/|
| * | Merge branch 'master' into no-shellBernhard Schommer2015-02-191-22/+34
| |\|
| * | Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-291-32/+56
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-231-1/+1
|\ \ \ | | |/ | |/|
| * | Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+1
| |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| | * | Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-1/+1
| | |/
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-121-21/+33
|\| | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | PR#16: give option rules precedence over file pattern rules.Xavier Leroy2015-01-031-22/+33
| | | | | | | | | | | | | | | | | | Plus: simplify handling of -help and --help. Plus: error on unrecognized "-xxx" options so that "-foo.c" is not treated as a source file.
| * | PR#14: recognize ".so" arguments as files to pass to the linker.Xavier Leroy2015-01-021-1/+2
| |/
* / Renamed the printer module for the Abbreviations and deactivated adding the ↵Bernhard Schommer2014-12-021-1/+1
|/ | | | -g option to the assembler.
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-241-1/+1
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-161-12/+29
| | | | them off.
* Revised parsing of command-line arguments (in preparation for adding more).Xavier Leroy2014-11-161-118/+104
| | | | | | Honor "ccomp -E foo.h" for GCC compatibility. Accept .o.ext files as object files for GCC compatibility. Fixed and improved handling of Cminor source files.
* Removed environment variable for the stdlib_path and added a new variable ↵Bernhard Schommer2014-10-061-5/+1
| | | | for the configuration file.
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-0/+1
|
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-191-4/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nicer reporting of I/O errors (e.g. "No such file").xleroy2014-08-131-23/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2564 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-2/+3
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-091-1/+1
| | | | | | | | | | over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-061-0/+2
| | | | | | | | | | | | | | | | | | | | | | | 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/+4
| | | | | | | | 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
* Recognize .i and .p source files as C sources not to be preprocessed.xleroy2014-02-051-3/+31
| | | | | | | Add CompCert version number and command line as comments in generated asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-20/+9
| | | | | | | - 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-3/+5
| | | | | | | | (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-2/+0
| | | | | | | | | | | | | | - 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
* Revised parsing of command-line options, more GCC-like.xleroy2013-12-211-21/+44
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-201-0/+3
| | | | 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-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2374 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compile in debug mode and activate stack backtraces.xleroy2013-07-071-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2292 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem ↵xleroy2013-05-171-0/+2
| | | | | | | | | 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-8/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* driver: removed option -flonglongxleroy2013-04-221-4/+2
| | | | | | | | test/c: added SHA3 cfrontend: support casts between long long and pointers, and comparisons between them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2213 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+4
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated PowerPC port to new integers.xleroy2013-02-121-1/+5
| | | | | | | Added options -falign-branch-targets and -falign-cond-branches (experimental). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2113 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Be more like gcc in the way we display or not the usage message.xleroy2013-02-121-8/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-3/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better treatment of volatile accesses in the reference interpreter.xleroy2013-01-081-2/+0
| | | | | | | Suppressed option -randvol. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2092 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 08:44:11 +0000