aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Update description for debugging optionsMichael Schmidt2016-10-141-4/+3
| | |
| * | Add a man-pageMichael Schmidt2016-10-143-0/+537
| | |
* | | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-4/+4
| | |
* | | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-3/+6
| | |
* | | Remove unnecessary usage of isatty.Bernhard Schommer2016-10-181-1/+1
| | |
* | | Catch errors from Unix for isatty.Bernhard Schommer2016-10-181-1/+4
| | | | | | | | | | | | | | | | | | There is a bug in the fstat implementation in ocaml 4.03 under windows. In order to prevent this we guard the isatty function with an additional try with.
* | | Document -target and -conf. Bug 20210Bernhard Schommer2016-10-181-0/+2
| | |
* | | Query menhir for location of menhir lib in config.Bernhard Schommer2016-10-182-38/+3
| | | | | | | | | | | | | | | | | | Since the menhir version required supports the --suggest-menhirLib flag we can query it already in the configure script simplifying the Makefile.menhir
* | | Refactored debugging options.Bernhard Schommer2016-10-143-31/+42
| | | | | | | | | | | | | | | | | | | | | The options controlling the generation of debugging information are now moved into the Debug module. Futhermore the -gdepth options are replaced in favor of a more gcc compatible version. Bug 20193
* | | Remove undocumented option. Bug 20193Bernhard Schommer2016-10-146-33/+10
|/ /
* | Fix minor typoMichael Schmidt2016-10-121-1/+1
| |
* | Added configure switch for merlin.Bernhard Schommer2016-10-061-0/+35
| | | | | | | | | | | | The new configure switch generates a .merlin file and adds the -bin-annot flag to the compile options. Bug 20081
* | Fixed regression in printing of floats.Bernhard Schommer2016-10-041-1/+1
|/ | | | | Commit 60402c5 breaks printing of default floats by adding support for %lf. This commit adds back support for %f.
* Keep anonymous members of anonymous structs.Bernhard Schommer2016-09-272-3/+5
| | | | | The anonymous members are kept but using them is still an error. Bug 19907
* 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
| | | | | | Now "expected at least %d" instead of "expected %d". Also improved error message for __builtin_debug. Bug 19872
* 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
| | | | | | | | The only case where compcert raise a pedantic warning was for implicit int parameters. This is the behavior of clang. However since not all other pedantic warnings are supported the behavior of gcc is adopted. Bug 19872.
* Allow %lf type specifier in printf.Bernhard Schommer2016-09-221-1/+1
| | | | | %lf is official part of the C99 standard. Bug 19877
* Reverted noisy change.Bernhard Schommer2016-09-221-1/+1
| | | | | | In order to empty declarations it is necessary to distinguish between forward declarations and empty declarations. Bug 19859
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-213-9/+13
|\ | | | | | | | | | | Fix minor issues in some proofs and tactics. Patch by Maxime Dénès.
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-213-9/+13
| | | | | | | | | | These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors.
* | 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
|\ \ | | | | | | Advanced diagnostics
| * | 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
| | | | | | | | | | | | | | | | | | Now the same warning is triggered for both cases, int to ptr and ptr to int. Bug 18004
| * | Fixed error message for & operator. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Added conformance warning.Bernhard Schommer2016-08-313-0/+4
| | | | | | | | | | | | | | | | | | This warning should be triggered if a feature is used that is not part of the code CompCert C language. Bug 18004
| * | Added back logical operator in error. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Reworded errors/warnings in Elab.Bernhard Schommer2016-08-311-60/+76
| | | | | | | | | | | | | | | | | | | | | | | | Some old errors/warnings messages were better before and are now rephrased. Furthermore some formulations are rephrased to match the used formulations of the ISO C stanard, e.g. storage class is replaced with storage-class. Bug 18004
| * | 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
| | | | | | | | | | | | | | | | | | Removed duplicated of, changed string to string literal for wording than the C standard. Bug 18004
| * | 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
| |\ \
generated by cgit (git 2.34.1) at 2024-07-05 06:45:19 +0000