| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
|
|
|
| |
Without scopes Coq 8.6 warns, probably rightly so.
|
|
|
|
| |
Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
|
|
|
|
|
| |
This silences a warning of Coq 8.6.
Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
|
|
|
|
|
| |
Open Local becomes Local Open. This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
|
| |
|
|
|
|
| |
This version of Flocq is compatible with Coq 8.6
|
|\
| |
| |
| | |
maximedenes-coq-8.6
|
| |
| |
| |
| | |
Menhir's Coq backend has been updated to support Coq 8.6.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
Not sure why, but it would be safer not to rely on automatic naming.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
In 64-bit mode jumptables contain differences of labels Lx-Ly.
The OS X assembler and linker have problems with those differences if the labels are from a given section (here, .text) and the difference is to be put in another section (previously, .const).
Putting the jumptables in .text fixes this issue, and is consistent with what is done for ELF.
|
| |
| |
| |
| | |
Minor performance tweak. Printf is more efficient for plain formats involving no boxes.
|
| |
| |
| |
| | |
I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
|
|\ \ |
|
| | | |
|
|/ /
| |
| |
| |
| |
| | |
The optional hex parameter only worked if the intconstant was also
of unsigned kind. Hence it is better to have one function in
Bitfields for this.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
Instead of exporting and setting all functions we just fill the
struct already in DebugInformation with the correct functions.
|
|\ \ \
| |/ /
|/| | |
|
| | |
| | |
| | |
| | |
| | | |
- Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type.
- Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce Cutil.class_of_attribute to return the class of the given attribute: one among
Attr_type attribute related to types (e.g. "aligned")
Attr_struct attribute related to struct/union/enum types (e.g. "packed")
Attr_function attribute related to function types (e.g. "noreturn")
Attr_name attribute related to variable and function declarations (e.g. "section")
Attr_unknown attribute was not declared
Cutil.declare_attribute is used to associate a class to a custom attribute.
Standard attributes (const, volatile, _Alignas, etc) are Attr_type.
cfronted/C2C.ml: declare the few attributes that CompCert honors currently.
cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
|
| | |
| | |
| | |
| | | |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
The Printf is only needed for the identifier functions.
Furthermore the new intconst from Cutil is used to generate the
integer constant and shadowing of the open C is removed.
|
| | |
| | |
| | |
| | |
| | | |
The intconst function comes with an optional parameter to add an
hex string for later printing.
|
| | |
| | |
| | |
| | | |
The clashing identifiers are now referenced explicitly.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
Locations are only used in two functions and can be referenced
there directly.
|
| | |
| | |
| | |
| | | |
The Locations are only used in one function.
|
| | |
| | |
| | |
| | | |
The two types needed from AST are prefixed directly.
|
| | | |
|
| | | |
|