aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into dwarfBernhard Schommer2015-01-1234-61988/+914
|\
| * In -g -S mode, annotate the generated asm file with the C source code in comm...Xavier Leroy2015-01-076-86/+243
| * PR#19: there is no reason to reject an empty "switch" statement.Xavier Leroy2015-01-061-2/+0
| * 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
| * PR#15: vararg functions are not eligible for inlining.Xavier Leroy2015-01-021-1/+1
| * Translation of wide string literals.Xavier Leroy2015-01-011-6/+57
| * Wrong handling of block-local function declarations (again)Xavier Leroy2015-01-011-12/+7
| * Revised type compatibility check w.r.t. handling of attributes.Xavier Leroy2015-01-014-49/+93
| * PR#12: regression introduced in commit 2d32afcXavier Leroy2014-12-301-2/+0
| * PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-305-9/+31
| * PR#11: support sizeof(struct {...}) and _Alignof(struct {...})Xavier Leroy2014-12-301-25/+38
| * Improve printing of errors.Xavier Leroy2014-12-301-3/+11
| * PR#10 continued: disambiguate record to avoid OCaml warningXavier Leroy2014-12-301-1/+1
| * PR#10: composite definitions must be maintained in the environment.Xavier Leroy2014-12-301-6/+15
| * cparser/Parser.v is generated.Xavier Leroy2014-12-301-0/+1
| * Recognize more of GCC's alternate keywords (e.g. "__signed").Xavier Leroy2014-12-291-21/+24
| * Support "asm volatile" (closes: PR#5).Xavier Leroy2014-12-292-1/+3
| * One more cleanup in configure.Xavier Leroy2014-12-181-1/+1
| * No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-184-61679/+15
| * Merge pull request #3 from AbsInt/pure-makefilesXavier Leroy2014-12-188-85/+371
| |\
| | * Minor bug fixes in configure and Makefile.extrXavier Leroy2014-12-172-5/+6
| | * Merge branch 'master' into pure-makefilesXavier Leroy2014-12-1759-763/+2379
| | |\ | | |/ | |/|
| | * Use OCaml's .opt compilers when available.Xavier Leroy2014-12-173-32/+82
| | * Remove ocamlbuild configuration files, no longer used.Xavier Leroy2014-11-222-23/+0
| | * Use String.map instead of reimplementing it ourselves.Xavier Leroy2014-11-221-5/+18
| | * Replace ocamlbuild by a second-stage makefile to compile the OCaml code and p...Xavier Leroy2014-11-225-59/+296
* | | Added dummy printing function for entries.Bernhard Schommer2014-12-181-1/+4
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-1710-58/+88
|\| |
| * | Clean up support for common symbols. Uninitialized "const" symbols can be co...Xavier Leroy2014-12-176-39/+71
| * | Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
| * | Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2014-12-175-19/+35
| |\ \
| | * | Stdlib path is ignored when the configuration has_runtime_lib is set to false.Bernhard Schommer2014-12-151-2/+7
| * | | Prototype the pointer so that the program has well defined semantics and pass...Xavier Leroy2014-12-171-1/+1
* | | | Added more printing code.Bernhard Schommer2014-12-151-3/+8
* | | | Started implementation of printing the dwarf entries.Bernhard Schommer2014-12-153-11/+31
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-114-17/+28
|\ \ \ \ | | |/ / | |/| |
| * | | Update the IA32/MacOS X port.Xavier Leroy2014-12-112-5/+7
| * | | Prevent constant propagation on Oindirectsymbol addresses.Xavier Leroy2014-12-111-2/+11
| * | | Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| |/ /
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-041-1/+0
|\| |
| * | Removed more unused variables.Bernhard Schommer2014-12-041-1/+0
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-042-6/+1
|\| |
| * | Removed unused variable and changed the search for the installation directory...Bernhard Schommer2014-12-042-6/+1
* | | Changed the d1line and d1file to d2line and d2file and prologue and epilogue ...Bernhard Schommer2014-12-045-9/+79
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-021-14/+7
|\| |
| * | Changed the comparison of jumptables.Bernhard Schommer2014-12-011-14/+7
* | | Renamed the printer module for the Abbreviations and deactivated adding the -...Bernhard Schommer2014-12-023-47/+11
* | | Merge branch 'master' into dwarfBernhard Schommer2014-11-2750-684/+2264
|\| |
| * | Wrong handling of block-local function declarations (in Elab.ml).Xavier Leroy2014-11-264-13/+31