| Commit message (Expand) | Author | Age | Files | Lines |
* | Merge branch 'master' of /common/repositories/git/tools/compcert | Bernhard Schommer | 2016-07-09 | 4 | -0/+68 |
|\ |
|
| * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_... | Michael Schmidt | 2016-07-08 | 2 | -0/+36 |
| * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_... | Michael Schmidt | 2016-07-08 | 2 | -0/+32 |
* | | Unwanted partial constant propagation in 64-bit integer arguments to builtins | Xavier Leroy | 2016-07-08 | 8 | -1/+18 |
* | | Port to Coq 8.5pl2 | Xavier Leroy | 2016-07-08 | 44 | -364/+540 |
|/ |
|
* | common/Determinism.v: dual-license with GPL | Xavier Leroy | 2016-06-30 | 2 | -14/+4 |
* | Changelog update: mention -g for ARM and IA32 | Xavier Leroy | 2016-06-30 | 1 | -0/+4 |
* | Merge branch 'master' of ssh://github.com/AbsInt/CompCert | Xavier Leroy | 2016-06-30 | 1 | -0/+1 |
|\ |
|
| * | Added back ;; | Bernhard Schommer | 2016-06-28 | 1 | -0/+1 |
* | | LICENSE: update the list of files that are dual-licensed under the GPL | Xavier Leroy | 2016-06-28 | 1 | -2/+10 |
|/ |
|
* | Activate advanced debug information for arm, ia32. | Bernhard Schommer | 2016-06-28 | 7 | -20/+5 |
* | bug 19234, inherit varargs flag from previous function definitions for KR con... | Michael Schmidt | 2016-06-28 | 1 | -4/+19 |
* | Merge pull request #103 from AbsInt/KR_fundefs | Bernhard Schommer | 2016-06-27 | 4 | -64/+171 |
|\ |
|
| * | Revised handling of old-style, K&R function definitions | Xavier Leroy | 2016-06-24 | 4 | -64/+171 |
* | | Merge pull request #102 from AbsInt/memory_permissions | Xavier Leroy | 2016-06-27 | 5 | -9/+154 |
|\ \ |
|
| * | | Stricter control of permissions in memory injections and extensions | Xavier Leroy | 2016-06-22 | 5 | -9/+154 |
| |/ |
|
* | | Also add braces for arm. Bug 19197 | Bernhard Schommer | 2016-06-24 | 1 | -2/+2 |
* | | Added braces back. Bug 19197 | Bernhard Schommer | 2016-06-24 | 1 | -16/+16 |
* | | Moved assembler and linker into own files. | Bernhard Schommer | 2016-06-24 | 9 | -122/+210 |
* | | Deactivate options target dependend. | Bernhard Schommer | 2016-06-24 | 2 | -110/+131 |
|/ |
|
* | Update in preparation for release 2.7 | Xavier Leroy | 2016-06-22 | 2 | -3/+49 |
* | Improved handling of "rotate left" and "rotate right" operators | Xavier Leroy | 2016-06-22 | 5 | -42/+73 |
* | Driveraux.mli: fix documentation comment | Xavier Leroy | 2016-06-22 | 1 | -1/+1 |
* | Remove code that will is deprecated in ocaml 4.03 | Bernhard Schommer | 2016-06-21 | 11 | -19/+29 |
* | Pass the updated env through elab_expr. | Bernhard Schommer | 2016-06-21 | 1 | -149/+166 |
* | fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can... | Michael Schmidt | 2016-06-07 | 4 | -4/+4 |
* | Fixed warning 45 for ExportClight.ml. | Bernhard Schommer | 2016-05-28 | 1 | -1/+1 |
* | Merge pull request #101 from fpottier/comment | Bernhard Schommer | 2016-05-27 | 2 | -5/+3 |
|\ |
|
| * | Fixed a comment. | François Pottier | 2016-05-27 | 2 | -5/+3 |
|/ |
|
* | Merge pull request #99 from AbsInt/register-pairs | Xavier Leroy | 2016-05-27 | 31 | -893/+870 |
|\ |
|
| * | ia32/Conventions1: remove commented-out proof attempt | Xavier Leroy | 2016-05-24 | 1 | -17/+0 |
| * | configure: regression on Menhir's minimal version | Xavier Leroy | 2016-05-24 | 1 | -1/+1 |
| * | Introduce register pairs to describe calling conventions more precisely | Xavier Leroy | 2016-05-17 | 32 | -894/+888 |
* | | Merge pull request #100 from AbsInt/driver-split | Xavier Leroy | 2016-05-27 | 9 | -509/+492 |
|\ \
| |/
|/| |
|
| * | Added version string to Clightgen. | Bernhard Schommer | 2016-05-24 | 2 | -3/+15 |
| * | Escape all newlines. | Bernhard Schommer | 2016-05-24 | 1 | -5/+5 |
| * | Moved shared frontend code in own file. | Bernhard Schommer | 2016-05-24 | 8 | -437/+356 |
| * | Moved some system functions into own module. | Bernhard Schommer | 2016-05-24 | 3 | -68/+120 |
|/ |
|
* | bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are rest... | Michael Schmidt | 2016-05-13 | 1 | -1/+2 |
* | Split dependency generation. | Bernhard Schommer | 2016-05-13 | 1 | -1/+2 |
* | Respect COQBIN in configure script. | Bernhard Schommer | 2016-05-13 | 1 | -1/+1 |
* | Added option to pass linker options to gcc. | Bernhard Schommer | 2016-05-13 | 1 | -0/+2 |
* | configure: bump Menhir required version to 20160303 | Xavier Leroy | 2016-05-11 | 1 | -1/+1 |
* | fix typo 'clinker_option' in configure for OSX | Michael Schmidt | 2016-05-10 | 1 | -2/+2 |
* | fix typo in comment | Michael Schmidt | 2016-05-10 | 1 | -1/+1 |
* | fix typo 'clinker_option' in configure for OSX | Michael Schmidt | 2016-05-10 | 1 | -6/+10 |
* | ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory... | Xavier Leroy | 2016-05-07 | 2 | -111/+141 |
* | Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a... | Xavier Leroy | 2016-04-27 | 25 | -2781/+2973 |
* | bug 18004, fix file extensions for dparse option | Michael Schmidt | 2016-04-25 | 2 | -2/+2 |
* | Enabled Werror via command line option. | Bernhard Schommer | 2016-04-25 | 1 | -0/+1 |