aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Expand)AuthorAgeFilesLines
* 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 separate...Bernhard Schommer2015-07-013-5/+5
* Added --version option to print version string.Bernhard Schommer2015-06-261-9/+19
* Merge pull request #43 from AbsInt/standard-headersXavier Leroy2015-06-083-2/+9
|\
| * Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-253-2/+9
* | Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-071-1/+1
* | Allow the option -o to be also the prefix of the file name for compability wi...Bernhard Schommer2015-05-311-0/+2
|/
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-1/+1
* Merge branch 'master' into dwarfBernhard Schommer2015-03-314-2/+116
|\
| * Improvements in the StructReturn transformation (ABI conformance for passing ...Xavier Leroy2015-03-205-19/+96
| * Merge branch 'master' into struct-passingXavier Leroy2015-03-143-189/+180
| |\
| * | Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-142-3/+29
| * | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-272-1/+10
* | | Added missing functions for printing the structs and unions. Still missing pr...Bernhard Schommer2015-03-241-8/+4
* | | 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
* | | Started implementing the printing functions for the debug info. Added a globa...Bernhard Schommer2015-03-161-0/+6
* | | Merge branch 'master' into dwarfBernhard Schommer2015-03-103-189/+180
|\ \ \ | | |/ | |/|
| * | Merge branch 'master' into no-shellBernhard Schommer2015-02-194-137/+113
| |\ \
| | * | Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-081-95/+61
| | |/
| * | Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-292-94/+119
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-232-12/+14
|\ \ \ | | |/ | |/|
| * | Merge branch 'named-structs'Xavier Leroy2015-01-232-12/+14
| |\ \
| | * | Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-222-11/+13
| | * | Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-1/+1
* | | | Merge branch 'master' into dwarfBernhard Schommer2015-01-123-30/+38
|\| | |
| * | | PR#16: give option rules precedence over file pattern rules.Xavier Leroy2015-01-033-31/+38
| * | | PR#14: recognize ".so" arguments as files to pass to the linker.Xavier Leroy2015-01-021-1/+2
| | |/ | |/|
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-171-2/+7
|\| |
| * | Stdlib path is ignored when the configuration has_runtime_lib is set to false.Bernhard Schommer2014-12-151-2/+7
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-041-1/+1
|\| |
| * | Removed unused variable and changed the search for the installation directory...Bernhard Schommer2014-12-041-1/+1
| |/
* / Renamed the printer module for the Abbreviations and deactivated adding the -...Bernhard Schommer2014-12-021-1/+1
|/
* Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-242-2/+9
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-1/+21
* Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-241-1/+2
* Add flags to control individual optimization passes + flag -O0 for turning th...Xavier Leroy2014-11-164-37/+116
* Revised parsing of command-line arguments (in preparation for adding more).Xavier Leroy2014-11-163-118/+250
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-131-1/+1
* Removed environment variable for the stdlib_path and added a new variable for...Bernhard Schommer2014-10-063-20/+20
* Change the way the tools like the linker, assembler, etc. are specified by in...Bernhard Schommer2014-09-301-0/+86
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-293-50/+64
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-192-5/+9
* Nicer reporting of I/O errors (e.g. "No such file").xleroy2014-08-131-23/+26
* configure: distinguish between ABI and processor model.xleroy2014-07-291-2/+2
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-2/+3
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-273-1/+5
* Merge of "newspilling" branch:xleroy2014-07-231-1/+1
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-1/+1
* Merge of branch linear-typing:xleroy2014-04-063-22/+78