| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
| |
cfrontend/C2C.ml
|
| | |
|
| |
|
|
| |
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
|
| |
|
|
| |
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.
|
