aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
| * | | | Additional test for color output.Bernhard Schommer2016-08-056-75/+102
| * | | | Classified all warnings and added various options.Bernhard Schommer2016-07-2916-358/+690
* | | | | IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-185-50/+187
* | | | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-173-31/+39
* | | | | Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
* | | | | Added option to specify sdump folder. Fix 19816.Bernhard Schommer2016-09-161-2/+7
* | | | | improve fixup code (bug 19792)Michael Schmidt2016-09-151-0/+2
* | | | | Add interference for indirect calls.Bernhard Schommer2016-09-155-6/+22
* | | | | Add missing fixup-code for ARM EABI (bug 19792)Michael Schmidt2016-09-141-2/+0
* | | | | add missing print operatorMichael Schmidt2016-09-141-0/+1
* | | | | Removed some implict arguments.Bernhard Schommer2016-09-053-33/+14
| |_|/ / |/| | |
* | | | Pass the environment of k&r param elaboration.Bernhard Schommer2016-08-291-8/+10
* | | | Fixed spelling mistake and unnamed fields.Bernhard Schommer2016-08-291-3/+6
* | | | Added check for duplicated members. Bug 19665Bernhard Schommer2016-08-291-0/+5
| |/ / |/| |
* | | Use old scope in after parameter parsing.Bernhard Schommer2016-08-261-1/+1
* | | Reuse types from parameters in function definitonsBernhard Schommer2016-08-253-41/+47
* | | Test if struct is redefined as union or otherwise.Bernhard Schommer2016-08-251-0/+2