| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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
|
| |
|
| |
|
|\
| |
| | |
Added the _Noreturn keyword.
|
| |
| |
| |
| |
| |
| |
| |
| | |
CompCert now recognizes the C11 _Noreturn function specifier and
emits a simple warning for functions declared _Noreturn containing
a return statement. Also the stdnoreturn header and additionally
the stdalign header are added.
Bug 18541
|
|/ |
|
| |
|
|
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|
|
|
|
|
|
|
|
|
|
| |
Since the menhir version we use requires ocaml>4.02 we can also
upgrade the required ocaml version to >4.02 and remove the
deprecate String functions.
Also we now activate all warnings except for 4,9 und 27 for regular
code plus a bunch of warnings for the generated code. 4 and 9 are
not really usefull and 27 is deactivated since until the usage
string is printed in a way that requires no newline.
Bug 18394.
|
|
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
|
|
|
|
|
| |
Compare the underlying array types, otherwise we end up in a
endless recursion.
Bug 18374
|
|
|
|
|
|
| |
Since we cannot construct a default initializer for void types
we need to exit earlier.
Bug 18004.
|
|
|
|
|
|
| |
In parse_int it was not tested if the value of v is smaller than
zero. This allowed it that certain large integers were accepted
due to wrap around.
|
|
|
|
|
| |
Implementing the same behavior as gcc anc clang.
Bug 18004
|
|
|
|
|
|
| |
The C standard specifies that an enum type should be compatible
to some integer type (ISO/IEC 9899:TC3 §6.7.2.2p4).
Fix 16692
|
|
|
|
|
|
|
|
|
|
| |
Some newlib headers use the __extension__ keyword which suppresses
warnings for gcc extensions in strict mode. CompCert now ignores
this keyword for the gnu backends.
Also it seems that stddef of the gcc defines wint_t even though
it should not. However some libs rely on this. So wint_t is now
defined in CompCert's stddef header.
Bug 17613.
|
|
|
|
|
|
| |
- Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing'
- Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful.
- Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
|
|
|
|
|
|
|
| |
Since the identifier of a function definition and of its declaration
are equal we only should remove functions if the function iteself is
removed.
Bug 17724.
|
|
|
|
|
|
| |
On windows opening files in text mode can result in errors due to
non-windows compatible input. Thus open files only in binary mode.
Bug 17664
|
| |
|
|
|
|
| |
This seems to agree with clang and with the emacs C mode.
|
| |
|
|
|
|
| |
and merging two error states into one. There should be no observable change.
|
| |
|
|
|
|
| |
Regression test added in regression/initializers.c
|
|\
| |
| | |
Parser : duplicate identifier tokens, fix K&R definition parsing
|
| | |
|
| |
| |
| |
| | |
handcrafted.messages
|