| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
| |
cfrontend/C2C.ml
|
| |
|
|
|
|
|
|
|
| |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
| |
|
|
|
|
| |
The warning should only be active if the optimization is active,
so the check is only performed when the warning is active and
additionally the command line flag -Obranchless is specified.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The new diagnostics is triggered if a conditional is used that
may not be transformed into linear code by the later by the
if conversion.
The new diagnostic is emitted if a conditional may contain an
unsafe expression or is contained within another conditional,
logical and or logical or expression. An expression is unsafe if
it contains a call, changes memory or if its evaluation leads to
undefined behavior, for example division and modulo.
Also fixes a small typo in a comment in Cutil.
|
| |
|
|
|
|
| |
Refactored the checks functions by using higher order traversal
functions for statements. Also introduce helper functions for the
traversal of initializers.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds a check to reject type definitions such as
```
typedef __attribute((section "foo")) int fooint;
```
GCC and Clang also reject this as an error.
Without the check, the behavior is somewhat surprising:
```
fooint x; // placed in section "foo"
fooint * x; // placed in default section, attribute "foo" is ignored
```
Note that the following must be accepted:
```
typedef struct { ... } __attribute((packed)) t;
```
The "packed" attribute is correctly attached to the struct type and should not be checked. This is achieved by using `attribute_of_type_no_expand` to get the attributes of the typedef-ed type, excluding the attributes carried by a struct/union or another typedef.
|
| |
|
|
|
|
| |
Parameters also need to be checkd for unknown attributes, like
all other declarations.
Bug 24277
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
|
|
|
| |
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
|
