| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
|
|
|
| |
`-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
|
|
|
|
|
|
| |
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
|
|
|
|
| |
alloctrace debug-output
|
|
|
|
|
|
| |
Instead of using Filename.quote, string entries are printed with
%S.
Bug 21216
|
|
|
|
|
|
| |
The compilation directory entry needs quoting since it could be
a toplevel directory under windows.
Bug 21216
|
|\
| |
| |
| |
| |
| |
| | |
Adapt proofs to future handling of literal constants in Coq
This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
|
| |
| |
| |
| |
| |
| | |
This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
|
|/ |
|
| |
|
|
|
|
|
|
|
| |
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.
|
|\
| |
| |
| | |
Treat as _Noreturn the standard C11 functions that are _Noreturn but not always declared as such in header files.
|
| | |
|
| | |
|
|/
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|\
| |
| | |
Introduced configuration variable for gnu systems.
|
| |
| |
| |
| |
| |
| |
| | |
The variable gnu_toolchain is true if a gnu toolchain is used and
false in all other cases. The variable avoids the explicit test
whether the system string is diab and should be easier to change.
Bug 20521.
|
|\ \
| | |
| | |
| | | |
Improved warnings related to function returns
|
| | |
| | |
| | |
| | | |
Plus: updated comments.
|
| | |
| | |
| | |
| | | |
The new implementation keeps track of goto labels that are actually branched to. It is less optimized than the previous implementation (no bit vectors) but perhaps easier to read.
|
| | |
| | |
| | |
| | | |
Those labeled statements can be entered either by fall-through or by the enclosing switch.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to
- warn for non-void functions that can return by falling through the body
- warn more precisely for _Noreturn functions that can return
- introduce the "return 0" in "main" functions less often (cosmetic).
For the control-flow analysis, the following conservative approximations are made:
- any "goto" label is reachable
- all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case)
- the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants.
|
| | |
| | |
| | |
| | | |
Follow-up to [29653ba]
|
|\ \ \
| | | |
| | | |
| | | |
| | | |
| | | | |
Remove CompCert's ability to parse and compile source files written in Cminor
This facility is no longer used (as far as we know) and is painful to maintain.
|
| | | | |
|
|/ / / |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
Without scopes Coq 8.6 warns, probably rightly so.
|
| | |
| | |
| | |
| | | |
Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
|
| | |
| | |
| | |
| | |
| | | |
This silences a warning of Coq 8.6.
Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
|
| | |
| | |
| | |
| | |
| | | |
Open Local becomes Local Open. This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
|
| | | |
|
| | |
| | |
| | |
| | | |
This version of Flocq is compatible with Coq 8.6
|