aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
Commit message (Collapse)AuthorAgeFilesLines
...
* Add the debug interface file.Bernhard Schommer2015-09-161-0/+1
| | | | | | | | The new file Debug.ml contains the interface for generating and printing debug information. In order to generate debug information the init function initializes the necessary functions depending on the -g flag. If the -g is not there all functions are dummy functions which do nothing.
* Merge branch 'new-builtins'Bernhard Schommer2015-09-011-2/+4
|\
| * Improve error reporting in Asmexpand.Xavier Leroy2015-08-241-2/+4
| |
* | Improve printing of internal compiler errors.Xavier Leroy2015-08-251-2/+2
| |
* | Fixed the -T option.Bernhard Schommer2015-08-251-1/+1
| | | | | | | | The diab compiler expected -Wm<pathname> without whitespace.
* | Count number of input files and do not use number of source files for ↵Bernhard Schommer2015-08-241-12/+14
| | | | | | | | warning about no input.
* | Added error message when no input file is specified.Bernhard Schommer2015-08-231-0/+5
|/
* Added command line option to specify a linker command file for the linker.Bernhard Schommer2015-08-201-0/+5
|
* Also print the system in the output to differentiate between diab and gcc ↵Bernhard Schommer2015-08-051-2/+2
| | | | produced code in later checks.
* Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-071-1/+3
|
* Merge branch 'master' into json_exportBernhard Schommer2015-07-061-10/+23
|\ | | | | | | | | Conflicts: driver/Driver.ml
| * Added Build, Tag, etc in version string and driver/Version.ml should be ignoredBernhard Schommer2015-07-011-1/+1
| |
| * Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-011-2/+5
| | | | | | | | separate file.
| * Added --version option to print version string.Bernhard Schommer2015-06-261-9/+19
| |
* | Merge branch 'master' into json_exportBernhard Schommer2015-06-171-2/+4
|\|
| * Merge pull request #43 from AbsInt/standard-headersXavier Leroy2015-06-081-2/+2
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge of the "standard-headers" branch. This provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h. These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries. So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses: 1- Diab C's stdarg.h is not compatible with CompCert 2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.
| | * Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
| * | 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
generated by cgit (git 2.34.1) at 2024-07-05 16:46:16 +0000