| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
| |
Before, we were doing C90, there was no official syntax for such attributes, and we used ours. With C99 we can use "ty [ attributes N ]" to print "array with attributes of N elements of type ty".
|
| |
|
|
|
|
|
| |
Owing to the peculiarities of array types in Cutil.change_attributes_type, type-related attributes of the array element type were duplicated on the array type. E.g. elaborating 'const int a[10][5]' produced
"a is an array of 5 const arrays of 10 const ints"
instead of
"a is an array of 5 arrays of 10 const ints"
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The treatment of attributes in the current CompCert is often surprising. For example,
attribute(xxx) char * x;
is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char".
CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e.
const char * x;
is really "x is a pointer to a const char", not "x is a const pointer to char".
This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above,
attribute(xxx) char * x; // "attribute(xxx)" applies to "x"
const char * x; // "const" applies to "char"
This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
|
| |
|
|
| |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
