| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
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
|
|\ \ \
| |_|/
|/| |
| | | |
maximedenes-coq-8.6
|
| | |
| | |
| | |
| | | |
Menhir's Coq backend has been updated to support Coq 8.6.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
Not sure why, but it would be safer not to rely on automatic naming.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
In 64-bit mode jumptables contain differences of labels Lx-Ly.
The OS X assembler and linker have problems with those differences if the labels are from a given section (here, .text) and the difference is to be put in another section (previously, .const).
Putting the jumptables in .text fixes this issue, and is consistent with what is done for ELF.
|
| | |
| | |
| | |
| | | |
Minor performance tweak. Printf is more efficient for plain formats involving no boxes.
|
| | |
| | |
| | |
| | | |
I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
|
|\ \ \ |
|
| | |/
| |/| |
|
|/ /
| |
| |
| |
| |
| | |
The optional hex parameter only worked if the intconstant was also
of unsigned kind. Hence it is better to have one function in
Bitfields for this.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
Instead of exporting and setting all functions we just fill the
struct already in DebugInformation with the correct functions.
|
|\ \ \
| |/ /
|/| | |
|
| | |
| | |
| | |
| | |
| | | |
- Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type.
- Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce Cutil.class_of_attribute to return the class of the given attribute: one among
Attr_type attribute related to types (e.g. "aligned")
Attr_struct attribute related to struct/union/enum types (e.g. "packed")
Attr_function attribute related to function types (e.g. "noreturn")
Attr_name attribute related to variable and function declarations (e.g. "section")
Attr_unknown attribute was not declared
Cutil.declare_attribute is used to associate a class to a custom attribute.
Standard attributes (const, volatile, _Alignas, etc) are Attr_type.
cfronted/C2C.ml: declare the few attributes that CompCert honors currently.
cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
|
| | |
| | |
| | |
| | | |
Before, we were doing C90, there was no official syntax for such attributes, and we used ours. With C99 we can use "ty [ attributes N ]" to print "array with attributes of N elements of type ty".
|