| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| | |
Advanced diagnostics
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
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
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Removed duplicated of, changed string to string literal for
wording than the C standard.
Bug 18004
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
lib/Integers.v: define division-remainder of a double word by a word
ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction
ia32/*: adapt accordingly
Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
|
| | | |
| | | |
| | | |
| | | | |
Inline directives in extraction.v make the Caml output efficient and almost nice.
|
| | | |
| | | |
| | | |
| | | | |
The cut-and-paste was for compatibility with Coq 8.4
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Avoids problems with overwritting the registe containing the
function address.
Bug 19779
|
| | | | |
|
| | | | |
|
| |_|/
|/| |
| | |
| | | |
Also changed Local Open to Open Local.
|
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
The test is extended for integer constants smaller than 0. Also the
default constant used for the error is no longer 0 since this is
not a positive number.
Bug 19629
|
|\ \
| | |
| | | |
Support for ARM Big Endian
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Instead of an addition -little or -big at the end the configure
script now accepts armeb* for the big endian arm targets.
Bug 19418
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The spilling strategy for 2-address operations was strange in the case where the first argument needs spilling but not (yet) the result: a Xreload instruction was generated which prevented future spilling of the result.
Fixed by generating Xmove instead of Xreload in this case.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The declarations of malloc and free should also be printed for
CompCert C.
Bug 19616.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|