aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Improve wording of normal backtrace case Bug 19872Bernhard Schommer2017-01-191-1/+3
|
* Use quoted strings.Bernhard Schommer2017-01-181-11/+12
| | | | | | Instead of escaping all newlines etc for the help options use quoted strings. Bug 19872
* More comments and improvements for unknown loc.Bernhard Schommer2017-01-182-1/+27
| | | | | | More functions are now documented. Furthermore compcert now prints "ccomp:" instead of nothing for unknown locations. Bug 19872
* Remove duplaceted relese. Bug 20681Bernhard Schommer2017-01-171-1/+1
|
* Added missing whitespace. Bug 19872Bernhard Schommer2017-01-171-1/+1
|
* Safe the backtrace earlier. Bug 20681Bernhard Schommer2017-01-171-12/+13
|
* Added backtrace handler.Bernhard Schommer2017-01-172-0/+19
| | | | | | | | If CompCert crashes because of an uncaught exception the exception is caught toplevel and the backtrace is printed plus an additional message to include the backtrace in a support request, if buildnr and tag are available. Bug 20681.
* Allow multiple nameless bit field fields.Bernhard Schommer2016-12-291-2/+4
|
* Merge pull request #153 from AbsInt/anonymous_struct2Bernhard Schommer2016-12-277-39/+113
|\ | | | | Next try for support of anonymous structs.
| * Avoid exception catch-allXavier Leroy2016-12-261-1/+1
| | | | | | | | "try ...; true with _ -> false" is dangerous if "..." raises unexpected exceptions such as Out_of_memory or Stack_overflow.
| * Cosmetic indentation changeXavier Leroy2016-12-261-5/+4
| |
| * Added code for initializers. Bug 20003Bernhard Schommer2016-12-121-1/+19
| |
| * Moved naming and changed names of aux functionsBernhard Schommer2016-12-121-16/+20
| | | | | | | | | | | | | | | | The naming of anonymous structs is performed by an additional step in elab_struct_or_union_info instead of in elab_field_group. Also the aux functions are renamed to access. Bug 20003
| * Next try for support of anonymous structs.Bernhard Schommer2016-12-077-41/+94
| | | | | | | | | | | | Instead of using idents the anonymous fileds get names of the for <anon>_c where c is a counter of all anonymous members. Bug 20003
* | Added warning for inline asm in sdump. Bug 20593Bernhard Schommer2016-12-142-0/+7
|/
* Use -Wno- instead of -Wno to deactivate warnings.Bernhard Schommer2016-12-061-1/+1
|
* Warning for C11 _Noreturn feature.Bernhard Schommer2016-11-221-4/+10
| | | | The warning for C11 features is now also triggered for _Noreturn.
* Warning for decls without name in composites.Bernhard Schommer2016-11-224-6/+15
| | | | | | The warning missing declarations is now also triggered for declarations without name in field lists of composite types if the declaration is not an anonymous composite or a bitfield member.
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-3/+3
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * cparser/PackedStructs: fix assertion that was wrong for 64-bit targetsXavier Leroy2016-10-241-1/+1
| |
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-2/+2
| | | | | | | | | | | | | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* | 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.
* | Remove undocumented option. Bug 20193Bernhard Schommer2016-10-143-25/+8
|/
* 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
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-231-2/+3
| | | | | | Now "expected at least %d" instead of "expected %d". Also improved error message for __builtin_debug. Bug 19872
* mention -Wall in help textMichael Schmidt2016-09-221-0/+1
|
* 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.
* 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-211-0/+1
|\ | | | | | | | | | | 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-211-0/+1
| | | | | | | | | | 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
| |
* | 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
| |
* | 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
|\ \