aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* x86-64 MacOS X supportXavier Leroy2016-10-116-31/+68
* Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-064-115/+112
* Regression: compile-time evaluation of ((struct s *)0)->fieldXavier Leroy2016-10-062-4/+7
* Fix some 32-bit regressionsXavier Leroy2016-10-042-15/+56
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-0429-25/+3031
* Remove usage of do.Bernhard Schommer2016-10-043-122/+121
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-024-31/+361
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-0222-203/+547
* Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-0131-1625/+4945
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-0116-752/+478
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-0176-2557/+4834
* Keep anonymous members of anonymous structs.Bernhard Schommer2016-09-272-3/+5
* undefine _Nullable to add some compatibility with macOS 10.12 SDKMichael Schmidt2016-09-231-1/+1
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-232-4/+10
* Catch case of zero in builtin debug.Bernhard Schommer2016-09-221-2/+2
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-09-221-0/+1
|\
| * mention -Wall in help textMichael Schmidt2016-09-221-0/+1
* | Added sizetyp for subarray bounds. Fix 19894Bernhard Schommer2016-09-223-21/+43
|/
* Added compcert-conformance to wall. Bug 19872Bernhard Schommer2016-09-221-0/+2
* Renamed pedantic to implicit-int.Bernhard Schommer2016-09-223-8/+9
* Allow %lf type specifier in printf.Bernhard Schommer2016-09-221-1/+1
* Reverted noisy change.Bernhard Schommer2016-09-221-1/+1
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-213-9/+13
|\
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-213-9/+13
* | Fix typo in option name. Bug 18004Bernhard Schommer2016-09-211-1/+1
* | Also warn for empty default declarations. Bug 18004Bernhard Schommer2016-09-211-1/+1
* | Make unnamed default + correct empty struct warning. Bug 18004Bernhard Schommer2016-09-212-2/+3
* | Allow empty alignment attribute. Bug 18004Bernhard Schommer2016-09-211-0/+1
* | Remove the duplicated :. Bug 18004Bernhard Schommer2016-09-211-3/+3
* | Ignore also ignores the argunment. Bug 18004Bernhard Schommer2016-09-202-2/+7
* | Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-2021-395/+781
|\ \
| * | Fixed typos and reverted error message. Bug 18004Bernhard Schommer2016-09-051-9/+9
| * | Readded parameter number. Bug 18004Bernhard Schommer2016-09-011-6/+6
| * | Reworded warning. Bug 18004Bernhard Schommer2016-09-011-6/+6
| * | Simplified int to pointer tests.Bernhard Schommer2016-09-012-16/+17
| * | Fixed error message for & operator. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Added conformance warning.Bernhard Schommer2016-08-313-0/+4
| * | Added back logical operator in error. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Reworded errors/warnings in Elab.Bernhard Schommer2016-08-311-60/+76
| * | Restored original bit-field warning. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Updated comment string. Bug 18004.Bernhard Schommer2016-08-312-3/+3
| * | Readded warning about ignored volatile. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Added missing literal. Bug 18004Bernhard Schommer2016-08-311-1/+1
| * | Fixed typos.Bernhard Schommer2016-08-311-8/+8
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-1/+1
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-4/+4
| * | Fixed types in Elab.ml. Bug 18004Bernhard Schommer2016-08-291-5/+5
| * | Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-8/+18
| |\ \
| * \ \ Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-2956-577/+1051
| |\ \ \
| * | | | Added raw printing of types without formatting.Bernhard Schommer2016-08-163-5/+11