| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
|
| |
This warning should be triggered if a feature is used that is not
part of the code CompCert C language.
Bug 18004
|
| |
|
|
|
|
|
|
|
|
| |
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
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
The environment where the types are inserted is passed back to
allow introducing structs in k&r parameters.
Bug 19668
|
| |
| |
| |
| |
| |
| | |
The previous fix for duplicated members was also triggered for
unnamed members.
Bug 19665
|
| | |
|
|\| |
|
| |
| |
| |
| |
| |
| | |
Not decrementing the scopes again after a parameter parsing
lead to other scoping problems.
Bug 19656.
|
| |
| |
| |
| |
| |
| | |
In order to allow introducing structs in parameter definitions the
environment must keep the type information.
Bug 19602
|
| |
| |
| |
| |
| |
| | |
If a declaration of a composite is encountered it is also tested
if the kind is equal.
Bug 19630.
|
| |\
| | |
| | | |
Support for ARM Big Endian
|
| | |\ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Adds support for the big endian arm targets by making the target
endianess flag configurable, adding support for the big endian
calling conventions, rewriting memory access patterns and adding
big endian versions of the runtime functions.
Bug 19418
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Since some incomplete types are allowed in initialization just
test whether the default initilization exists.
Bug 19601
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
New types introduced in casts are now inserted into the right
Environment and carried along.
Bug 19614.
|
| | | |
| | | |
| | | |
| | | | |
This reverts commit c64c4ab2526ad87a3506c9e1fdf31fa1446c16eb.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Allows adding struct definitions in function parameters.
Bug 19602.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Initializers for function variables are not allowed. CompCert now
reports an error and exits.
Bug 19606
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Before the initializazion is computed we check wether the type is
incomplete.
Bug 19601
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
CompCert now reports an error for usage of the va_start macro in
non variadic functions.
Bug 19600.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Parameters also need to be checked for incomplete types.
Bug 19596
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Alginof and sizeof applied to incomplete types now exit earlier
with a fatal error.
Bug 19594.
|
| | |/
| |/|
| | |
| | |
| | |
| | | |
This allows problems in elaboration of the initializers for
variables of void type.
Bug 19577.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Instead of a warning for an empty union CompCert reports an error
and exits. This avoids problems during the generation of
initializers for these.
Bug 19565.
|
| | |
| | |
| | |
| | |
| | |
| | | |
The exception Wrong_attr_arg raised is now catched during the
translation of the wrong _Alignas attributes.
Bug 19568.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Added a check for errors after the elab phases to avoid problems
in the transformations due to broken input programs.
Bug 19504
|
| |/
| |
| |
| |
| |
| | |
Return with a expression that is not compatible with the given return type
of a function now causes and fatal error, to avoid problems with later
transformation passes depending on it.
|
| |
| |
| |
| |
| |
| | |
This avoids introducing line breaks during printing of function
types.
Bug 18004
|
| |
| |
| |
| |
| |
| | |
Color output is only enabled if stderr is a tty, and the
environment variable TERM is not empty or dumb.
Bug 18004
|
|/
|
|
|
|
|
|
|
|
| |
Now each warning either has a name and can be turned on/off, made
into an error,etc. or is a warning that always will be triggered.
The message of the warnings are similar to the ones emited by
gcc/clang and all fit into one line.
Furthermore the diagnostics are now colored if colored output is
available.
Bug 18004
|
| |
|
|
|
|
|
|
| |
In a call such as "f(expr, ..., expr)", if the identifier "f" is not declared, declare it as specified in the ISO C90 standard, namely like "extern int f()" would do it. Previously, the declaration was done "on the side" and not properly recorded in the environments.
The diff is relatively large because the "enter_or_refine_ident" had to be moved up in the file.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, CompCert incorrectly handles 'extern' and function
declarations within a block. For example:
int main(void)
{
{
extern int i;
i = 0;
}
{
extern float i;
i = 10;
}
}
CompCert fails to detect the inconsistent declarations of "i" in the
two blocks, simply because the first declaration is not in scope when
the second declaration is processed.
This commit changes the elaboration of file-scope declarations,
block-scope "extern" declarations and block-scope function
declarations so that they are checked against possible earlier
declarations found in the already-elaborated top-level declarations,
instead of in the current typing environment.
Owing to the lifting of block-scoped extern and static declarations to
the top-level already performed by the elaboration pass, the
already-elaborated top-level declarations give an accurate view of the
declarations of variables with internal or external linkage already
encountered and processed, even if they are not currently in scope.
|
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
|
|
|
| |
conversion
|
|
|
|
|
|
|
|
| |
This commits handles the case where the argument is passed with a type different from the actual type of the argument, as in
float f (x) float x; { return x; }
"x" is passed with type "double", and must be converted to "float" at the beginning of the function.
|
|
|
|
|
|
|
|
| |
Most of the code can be String.uppercase usages can either be
replaced by a more specialized version of coqstring_of_camlstring
(which is also slightly more effecient) or by specialized checks
that reject wrong code earlier.
Bug 19187
|
|
|
|
|
|
| |
Since casts, sizeof, etc. expressions can introduce new types
we also need to add these to the environment and pass it through.
Bug 17814
|
| |
|
|
|
|
| |
(§6.7.8), bug 18000
|
|
|
|
| |
(§6.7.8), bug 18000
|
| |
|
|
|
|
| |
strings, bug 18000
|