| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
|
|
|
|
|
|
| |
The ISO C99 standard allows cast only if the type name involved
is either a void type or a scalar type.
For compatibility with GCC and Clang we used to support casting
a struct or union to exactly the same struct or union type.
That does not seem useful in practice and complicates conformance
testing. This commit gets rid of this exception to the C99 rule.
Bug 23310
|
|
|
|
|
| |
Instead of overwriting the initializer of the anonymous member we
should just keep it.
Bug 23353
|
|
|
|
|
|
|
| |
Sizeof and _Alignof are not allowed on bit-fields
Sizeof and _Alignof are not allowed to be applied to a expression
that designates a bit-field member.
Bug 23311
|
|
|
| |
Unions containing multiple bit fields were transformed incorrectly.
|
|
|
|
|
|
|
| |
Arrays should decay to pointers except if they are used as operands of sizeof, _Alignof or as
operand of the unary &. The "comma" sequencing operator was missing a "decay" on the type of its second argument. All other operators "decay" their operands correctly.
Bug 23299
Bug 23311
|
|
|
|
|
|
| |
If an anonymous bit-field member is declared wrong, i.e. a wrong
type is used or a too large size is used the error message now
prints <anonymous> instead of an empty string.
Bug 23292
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Do not allow inline on main().
The C99 standard says that in a hosted environment inline shall
not appear in a declaration of main.
Bug 23274
* Added warning for _Noreturn on main().
The C11 standard does not allow any function specifier on the
main function.
Bug 23274
|
|
|
|
|
| |
struct/union arguments to annotations should not be transformed at top level,
but the regular function calls contained within must be transformed recursively.
|
|
|
|
|
|
|
| |
In order to ensure that no transformation for arguments to
builtin annotations are used, the original unchanged arguments are
used.
Bug 23179
|
|
|
|
|
|
|
| |
This should help with parallel builds, which currently fail sometimes
owing to a lack of a dependency on pre_parser_aux.cmi.
Also: move documentation comments from the .ml to the .mli
|
|
|
|
|
|
|
|
|
|
|
|
| |
Make sure struct/union arguments to __builtin_annot and related
builtins are always passed by reference using the default passing mode,
regardless of the ABI for passing struct/unions to "real" functions.
This ensures portability of annotations across ABIs, and avoids mismatches
between the annotation text and the actual number of arguments
(when a struct/union argument is passed as N integer arguments).
A similar special case already existed for __builtin_va_arg.
|
|
|
|
|
|
|
|
| |
Include the format specifier in error message when available in
order to make it easier to spot the broken ais parameter.
Futhermore introduce a new warning for unused ais parameters.
Bug 22464
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
|
| |
|
| |
|
|
|
|
|
|
| |
Since the used configuration for passing and returning values
struct values is pretty much static it can be hardwired into the
machine settings.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
|
|
|
|
|
|
|
|
|
|
| |
Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent.
This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
which is not in lib/
|
|
|
|
|
| |
This time with the correct place for setting the destination files.
Bug 20521
|
|
|
|
|
|
| |
* Do not pass the env back from for stmt decls.
This is the source of issue #211, the environment from the elaboration of
the declaration and expressions in the for loop should not be passed back.
|
| |
|
|
|
|
|
|
|
| |
In order to correctly support the noinline attribute we must store
whether the function was specified with an inline specifer, had
a noinline attribute or nothing.
Bug 22642
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Check recursively for const for modifiable lvalues
According to 6.3.2.1 a modifiable lvalue is an lvalue that does
have a const-qualified type, and if it is a union or structure it
does not have any member, including any member of all contained
strutures or union, with a const-qualified type.
The new check for modifiable lvalue additionally checks this now
instead of only testing for toplevel const.
Bug 22420
|
|
|
|
| |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
| |
|
|
|
|
|
|
|
|
| |
BigNumPrelude will soon leave Coq stdlib with the rest of the bignum
library (apart from Int31 files) to become a separate package.
With this (very minor) patch, Compcert compiles with or without
the hints declared in BigNumPrelude.
|
|
|
|
|
|
|
| |
The redefinition of a composite with a different tag type is now
a fatal error. This should avoid problems when the composite is
used.
Bug 21542
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
This port required the following additional changes:
- Integers: More properties about shrx
- SelectOp: now provides smart constructors for mulhs and mulhu
- SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
- Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
- test/: add SIMU make variable to run tests through a simulator
- test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
commit da14495c01cf4f66a928c2feff5c53f09bde837f
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu Apr 13 17:36:10 2017 +0200
RISC-V port, continued
Now working on Asmgen.
commit 36f36eb3a5abfbb8805960443d087b6a83e86005
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed Apr 12 17:26:39 2017 +0200
RISC-V port, first steps
This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
|
|
|
|
|
|
| |
If the label is on a different line than the code we can still
emit a line directive for the label.
Bug 21232
|
| |
|
|
|
|
|
|
|
| |
Since before a case statement is potentially unreachable code due
to break, etc. it is better to skip printing line information
directly before the case statement and print it afterwards.
Bug 21232
|
|
|
|
|
|
|
| |
The check tests whether the size calculation of an array overflows
or the array covers half of the available address space and reports
an error in this case.
Bug 21034
|
|
|
|
| |
The noinline attribute prevents functions from inlining.
|
|
|
|
|
|
|
|
|
| |
The attribute unused can be used to indicate if a variable or
parameter is unused and no warning should be emitted for it.
Furthermore this commit simplifies the check by adding a generic
function to traverse the program.
Bug 19872
|
|
|
|
|
|
|
|
|
| |
The unused variable check now uses two passes. One to collect the
used variables and one to report the unused variables.
Futhermore attribute checks are extended to composite declaration.
Also the check is now performed after elaboration.
Bug 19872
|
|
|
|
|
|
| |
The test now also checks whether the parameter are used at all in
the function body.
Bug 19872
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The check test whether the identifier is used at all in the
function and if not issue a warning. It is not tested whether the
usage is reachable at all, so
int i;
if (0)
i;
would not generate a warning. This is the same as gcc/clang does.
The warning is disabled per default, but is active if -Wall is
given.
Bug 19872
|
|
|
|
|
|
| |
There should not be a single check place, since for example
unknonw attributes should be check after elaboration and other
simplifications.
|
| |
|
|
|
|
|
|
|
| |
The new module adds a function which is called during parse after
all C transformation have taken place for adding additional
checks. Currently only unknown attribute are checked.
Bug 19872
|
|
|
|
|
|
| |
As a cosmetic optimization enabled by the static analysis in Cflow, we used to not insert a 'return 0' at end of 'main' if the body of 'main' cannot fall through.
Since this optimization is cosmetic (the back-end will remove the 'return 0' if unused) and since we don't fully trust this static analysis, revert this optimization and always insert 'return 0'.
|
|
|
|
| |
If no 'default' case appears in a 'switch', one is implicit at the end of the switch body, making possible to have a fall-through behavior.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The C11 standard declares exit,abort,_Exit,quick_exit and
thrd_exit as _Noreturn however this is not included in older C
libs and leads to false negatives in reporting _Noreturn and
return type warnings. This can be avoided by enhancing the
noreturn check of the Cflow analysis to also test if one of the
above functions is called.
Bug 21009
|
|
|
|
|
|
| |
Instead of changing the definition of sizeof we now ignore errors
raise in the Cflow module.
Bug 21005
|
|
|
|
|
|
|
|
| |
Since the function environment does not necessary contain structs
and unions defined in sizeof expressions the evaluation should be
not constant and the Environment excpetions should be catched.
Fix 21005
|
|\
| |
| |
| | |
Improved warnings related to function returns
|
| |
| |
| |
| | |
Plus: updated comments.
|