| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
Follow-up to commit 1df1830
|
|
|
|
| |
Those three functions can be useful to implement front-ends for languages other than C.
|
|
|
|
|
|
|
|
|
| |
The new option -fdiagnostics-format allows it to switch between
the three different format version:
-ccomp (default) with file:line:
-vi with file+line:
-msvc with file(line):
Bug 19872
|
| |
|
|
|
|
|
|
| |
Controls whether the [-Woption] is printed in the diagnostic
message for mappable warnings/errors.
Bug 19872
|
|
|
|
|
|
|
| |
The option -fmax-errors limits the number of errors that are
reported before the compilation is aborted. The default 0 means no
limit.
Bug 19872
|
| |
|
| |
|
|
|
|
|
|
| |
Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
|
|
|
|
|
|
| |
More functions are now documented. Furthermore compcert now prints
"ccomp:" instead of nothing for unknown locations.
Bug 19872
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|\
| |
| | |
Next try for support of anonymous structs.
|
| |
| |
| |
| | |
"try ...; true with _ -> false" is dangerous if "..." raises unexpected exceptions such as Out_of_memory or Stack_overflow.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| | |
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
|
|/ |
|
| |
|
|
|
|
| |
The warning for C11 features is now also triggered for _Noreturn.
|
|
|
|
|
|
| |
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.
|
|\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| | |
|
| |
| |
| |
| |
| |
| | |
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.
|
|/ |
|
|
|
|
|
| |
The anonymous members are kept but using them is still an error.
Bug 19907
|
|
|
|
|
|
| |
Now "expected at least %d" instead of "expected %d". Also improved
error message for __builtin_debug.
Bug 19872
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
In order to empty declarations it is necessary to distinguish
between forward declarations and empty declarations.
Bug 19859
|
|\
| |
| |
| |
| |
| | |
Fix minor issues in some proofs and tactics.
Patch by Maxime Dénès.
|
| |
| |
| |
| |
| | |
These minor problems were revealed by porting CompCert to Coq 8.6, where
they trigger errors.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Now the same warning is triggered for both cases, int to ptr and
ptr to int.
Bug 18004
|
| | |
|
| |
| |
| |
| |
| |
| | |
This warning should be triggered if a feature is used that is not
part of the code CompCert C language.
Bug 18004
|