aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cutil.ml
Commit message (Collapse)AuthorAgeFilesLines
* Added check for large arrays.Bernhard Schommer2017-02-211-0/+11
| | | | | | | 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
* Added handling for noreturn std functions.Bernhard Schommer2017-02-161-0/+4
| | | | | | | | | | 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
* Reverted changes in Cutil and catch in Cflow.Bernhard Schommer2017-02-161-17/+4
| | | | | | Instead of changing the definition of sizeof we now ignore errors raise in the Cflow module. Bug 21005
* Fixed problem with local structs/unions in Cflow.Bernhard Schommer2017-02-161-4/+17
| | | | | | | | 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
* Merge pull request #162 from AbsInt/return-analysis-2Xavier Leroy2017-02-151-21/+0
|\ | | | | | | Improved warnings related to function returns
| * More precise warnings about function returnsXavier Leroy2017-02-071-21/+0
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Revert broken change to Cutil.Bernhard Schommer2017-02-081-6/+2
|/ | | | | | 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.
* Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-061-6/+32
|\
| * Refactor the classification of attributesXavier Leroy2017-02-031-12/+32
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Revised elaboration of attributesXavier Leroy2017-01-311-0/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* | Generalized function to allow adding hex strings.Bernhard Schommer2017-02-061-2/+6
| | | | | | | | | | The intconst function comes with an optional parameter to add an hex string for later printing.
* | Improve indentation.Bernhard Schommer2017-01-311-1/+1
| |
* | New version to support designators.Bernhard Schommer2017-01-241-8/+5
| | | | | | | | | | | | | | | | | | The c standard allows member designators for offsetof. The current implementation works by recursively combining the offset of each of the member designators. For array access the size of the subtypes is multiplied by the index and for members the offset of the member is calculated. Bug 20765
* | Simplified version.Bernhard Schommer2017-01-201-33/+18
| | | | | | | | | | | | | | | | The problem was that sub structs are were not correctly aligned. The new version is much simpler and uses the sizeof_struct to calculate the individual offsets and add them up to get correct offest. Bug 20765
* | Implement offsetof via builtin.Bernhard Schommer2017-01-201-0/+37
|/ | | | | | | | | | | | The implementation of offsetof as macro in the form ((size_t) &((ty*) NULL)->member) has the problem that it cannot be used everywhere were an integer constant expression is allowed, for example in initiliazers of global variables and there is also no check for the case that member is of bitifield type. The new implementation adds a builtin function for this which is replaced by an integer constant during elaboration. Bug 20765
* Next try for support of anonymous structs.Bernhard Schommer2016-12-071-4/+5
| | | | | | Instead of using idents the anonymous fileds get names of the for <anon>_c where c is a counter of all anonymous members. Bug 20003
* Warning for decls without name in composites.Bernhard Schommer2016-11-221-0/+5
| | | | | | The warning missing declarations is now also triggered for declarations without name in field lists of composite types if the declaration is not an anonymous composite or a bitfield member.
* Simplified int to pointer tests.Bernhard Schommer2016-09-011-1/+2
| | | | | | Now the same warning is triggered for both cases, int to ptr and ptr to int. Bug 18004
* Updated comment string. Bug 18004.Bernhard Schommer2016-08-311-1/+1
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-2/+3
|\
| * Fix for initialization of incomplete typesBernhard Schommer2016-08-231-2/+3
| | | | | | | | | | | | Since some incomplete types are allowed in initialization just test whether the default initilization exists. Bug 19601
* | Classified all warnings and added various options.Bernhard Schommer2016-07-291-5/+13
|/ | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* Added the _Noreturn keyword.Bernhard Schommer2016-03-231-0/+21
| | | | | | | | CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-28/+28
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Code cleanup.Bernhard Schommer2016-03-101-32/+31
| | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Fixed typo in equal types.Bernhard Schommer2016-03-101-1/+1
| | | | | | Compare the underlying array types, otherwise we end up in a endless recursion. Bug 18374
* Make void always incomplete and exit on void members.Bernhard Schommer2016-02-021-1/+6
| | | | | | Since we cannot construct a default initializer for void types we need to exit earlier. Bug 18004.
* Allow adding of attributes in valid_assignment_attr.Bernhard Schommer2016-01-281-2/+2
| | | | | Implementing the same behavior as gcc anc clang. Bug 18004
* Enum is compatible to its integer type.Bernhard Schommer2015-12-171-0/+3
| | | | | | The C standard specifies that an enum type should be compatible to some integer type (ISO/IEC 9899:TC3 §6.7.2.2p4). Fix 16692
* Remove debug stmts during grouping of switch.Bernhard Schommer2015-11-061-4/+12
| | | | | | | Debug statements introduced during the translation result in warnings when they are introduced at the head of the switch. Since they are not used and the warning is not necessary we can remove them before. Fix 17580.
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-19/+19
|
* Move strip functions to Cutil.Bernhard Schommer2015-10-121-0/+42
| | | | | | Since the strip functions might be useful in other context and is more general then the debug information. Bug 17392.
* Allow redefinition of a typedef with the same name.Bernhard Schommer2015-10-041-0/+36
| | | | | C11 allows a typedef redefinition if the types are the same. We now allow this also and issue a warning and an error if the types are different.
* Move more functionality in the new interface.Bernhard Schommer2015-09-161-1/+20
| | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-071-1/+2
|
* Detect and reject "&" operator applied to "register" local variable or to a ↵Xavier Leroy2015-04-281-0/+13
| | | | bit field.
* Extended inline asm: handle missing cases.Xavier Leroy2015-04-281-2/+8
| | | | | | Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests.
* "ecomma" smart constructor: reassociate to the left so that it prints more ↵Xavier Leroy2015-03-201-2/+8
| | | | nicely.
* ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-271-0/+70
| | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-221-20/+12
| | | | | | | | | | | | | Several definitions in Cutil and elsewhere were accessing the default value of !Machine.config, before it is properly initialized in Driver. Delay evaluation of these definitions, and initialize Machine.config to nonsensical values so that lack of initialization is caught early (e.g. in Cutil.find_matching_*_kind). Also, following up on commit [3b8a094], don't use "wchar_t" typedef to type wide string literals, even if this typedef is in scope. The risk here is to hide an inconsistency between "wchar_t"'s definition in standard headers and CompCert's built-in definition.
* Revised type compatibility check w.r.t. handling of attributes.Xavier Leroy2015-01-011-35/+61
| | | | | | | We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively. In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary. Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do. Net result is fewer warnings and type-checking that is closer to GCC/Clang.
* PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-301-3/+15
| | | | | | | | | | - cparser/Machine indicates whether wchar_t is signed or not (it is signed int in Linux and BSD, but unsigned short in Win32) - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t" exists in the environment (e.g. after #include <stddef.h>). Only if wchar_t is not defined do we use the default from Machine. - Permit initialization of any integer array from a wide string literal, not just an array of wchar_t.
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-211-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean-up pass on C types:xleroy2014-04-231-5/+15
| | | | | | | | | | | | | - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* C: Support array initializers that are too short + default init for remainder.xleroy2014-03-281-0/+28
| | | | | | | | Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab.ml: more warnings.xleroy2013-12-301-2/+7
| | | | | | | Cutil.ml: fix sizeof calculation of structs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-1/+1
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bring sizeof and alignof in sync with cfrontend/Ctypes.xleroy2013-12-111-22/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2378 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, ↵xleroy2013-11-061-9/+18
| | | | | | and to avoid wasting global variable space by inflating their sizeof needlessly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2362 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-051-0/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 15:00:03 +0000