aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Added -dall which enables all tracing.Bernhard Schommer2016-08-021-0/+12
* Use asprintf instead of printing to a buffer.Bernhard Schommer2016-07-261-5/+2
* test/raytracer: use our own strdup(), since this is not a standard functionXavier Leroy2016-07-241-1/+9
* Updates to the local test suiteXavier Leroy2016-07-2424-187/+133
* Merge pull request #109 from AbsInt/extern-scopesBernhard Schommer2016-07-221-54/+104
|\
| * Nicer error message for redefinitions with incompatible typeXavier Leroy2016-07-221-3/+4
| * Improved handling of C90 calls to undeclared functionsXavier Leroy2016-07-211-73/+75
| * Revised handling of block-scoped extern declarationsXavier Leroy2016-07-211-46/+93
|/
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-07-181-2/+8
|\
| * Update Changelog for release 2.7.1v2.7.1Xavier Leroy2016-07-181-2/+8
* | Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-07-113-21/+32
|\|
| * Merge pull request #105 from m-schmidt/masterXavier Leroy2016-07-113-21/+32
| |\
| | * add 'runtime' token to lexerMichael Schmidt2016-07-011-0/+1
| | * extend cminor parser to accept "extern runtime" declarationsMichael Schmidt2016-07-011-0/+4
| | * add missing asmexpand step to cminor handler in driverMichael Schmidt2016-07-011-21/+27
* | | Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-07-094-0/+68
|\ \ \ | |/ / |/| |
| * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_...Michael Schmidt2016-07-082-0/+36
| * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_...Michael Schmidt2016-07-082-0/+32
| |/
* | Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-088-1/+18
* | Port to Coq 8.5pl2Xavier Leroy2016-07-0844-364/+540
|/
* common/Determinism.v: dual-license with GPLXavier Leroy2016-06-302-14/+4
* Changelog update: mention -g for ARM and IA32Xavier Leroy2016-06-301-0/+4
* Merge branch 'master' of ssh://github.com/AbsInt/CompCertXavier Leroy2016-06-301-0/+1
|\
| * Added back ;;Bernhard Schommer2016-06-281-0/+1
* | LICENSE: update the list of files that are dual-licensed under the GPLXavier Leroy2016-06-281-2/+10
|/
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-287-20/+5
* bug 19234, inherit varargs flag from previous function definitions for KR con...Michael Schmidt2016-06-281-4/+19
* Merge pull request #103 from AbsInt/KR_fundefsBernhard Schommer2016-06-274-64/+171
|\
| * Revised handling of old-style, K&R function definitionsXavier Leroy2016-06-244-64/+171
* | Merge pull request #102 from AbsInt/memory_permissionsXavier Leroy2016-06-275-9/+154
|\ \
| * | Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-225-9/+154
| |/
* | Also add braces for arm. Bug 19197Bernhard Schommer2016-06-241-2/+2
* | Added braces back. Bug 19197Bernhard Schommer2016-06-241-16/+16
* | Moved assembler and linker into own files.Bernhard Schommer2016-06-249-122/+210
* | Deactivate options target dependend.Bernhard Schommer2016-06-242-110/+131
|/
* Update in preparation for release 2.7Xavier Leroy2016-06-222-3/+49
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-225-42/+73
* Driveraux.mli: fix documentation commentXavier Leroy2016-06-221-1/+1
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-2111-19/+29
* Pass the updated env through elab_expr.Bernhard Schommer2016-06-211-149/+166
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can...Michael Schmidt2016-06-074-4/+4
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
* Merge pull request #101 from fpottier/commentBernhard Schommer2016-05-272-5/+3
|\
| * Fixed a comment.François Pottier2016-05-272-5/+3
|/
* Merge pull request #99 from AbsInt/register-pairsXavier Leroy2016-05-2731-893/+870
|\
| * ia32/Conventions1: remove commented-out proof attemptXavier Leroy2016-05-241-17/+0
| * configure: regression on Menhir's minimal versionXavier Leroy2016-05-241-1/+1
| * Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-1732-894/+888
* | Merge pull request #100 from AbsInt/driver-splitXavier Leroy2016-05-279-509/+492
|\ \ | |/ |/|
| * Added version string to Clightgen.Bernhard Schommer2016-05-242-3/+15