aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cutil.mli
Commit message (Collapse)AuthorAgeFilesLines
* Revert broken change to Cutil.Bernhard Schommer2017-02-081-2/+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-2/+19
|\
| * Refactor the classification of attributesXavier Leroy2017-02-031-4/+19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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/+2
| | | | | | | | | | The intconst function comes with an optional parameter to add an hex string for later printing.
* | Avoid overflows and report an error.Bernhard Schommer2017-01-311-0/+3
| | | | | | | | | | | | | | Instead of multiplying the array constant directly with the size of the offset the cautious_mul function is used to detect potential overflows. Bug 20765
* | New version to support designators.Bernhard Schommer2017-01-241-1/+1
| | | | | | | | | | | | | | | | | | 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
* | Implement offsetof via builtin.Bernhard Schommer2017-01-201-0/+3
|/ | | | | | | | | | | | 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
* Warning for decls without name in composites.Bernhard Schommer2016-11-221-0/+2
| | | | | | 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.
* Updated comment string. Bug 18004.Bernhard Schommer2016-08-311-2/+2
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-0/+2
|\
| * Fix for initialization of incomplete typesBernhard Schommer2016-08-231-0/+2
| | | | | | | | | | | | 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-0/+3
|/ | | | | | | | | | 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/+5
| | | | | | | | 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
* Code cleanup.Bernhard Schommer2016-03-101-3/+1
| | | | | | 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.
* Remove debug stmts during grouping of switch.Bernhard Schommer2015-11-061-0/+2
| | | | | | | 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-2/+2
|
* Move strip functions to Cutil.Bernhard Schommer2015-10-121-0/+4
| | | | | | 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/+2
| | | | | 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-0/+2
| | | | | | 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.
* Detect and reject "&" operator applied to "register" local variable or to a ↵Xavier Leroy2015-04-281-0/+4
| | | | bit field.
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-0/+9
|\ | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-271-0/+9
| | | | | | | | | | | | | | | | | | | | 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.
* | Added translation fucntion for declarations and fundefinitions.Bernhard Schommer2015-03-231-0/+2
|/
* Merge branch 'named-structs'Xavier Leroy2015-01-231-2/+4
|\ | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-2/+4
| | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
* | Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-221-6/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | 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-4/+20
| | | | | | | | | | | | | | 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-1/+1
|/ | | | | | | | | | - 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.
* Clean-up pass on C types:xleroy2014-04-231-0/+2
| | | | | | | | | | | | | - 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/+5
| | | | | | | | 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
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, ↵xleroy2013-11-061-1/+1
| | | | | | 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/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize attribute((packed)) after a "struct {...}" and not just between ↵xleroy2013-06-211-0/+2
| | | | | | "struct" and "{", for compatibility with GCC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+3
| | | | | | | cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp: help debug stuck expressionsxleroy2012-02-101-0/+2
| | | | | | | | StructReturn: was building an ill-typed Ecomma expression Cutil: export "ecast" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1816 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: don't generate "vfd" directive, useless?xleroy2011-08-221-1/+3
| | | | | | | cparser: distinguish more carefully between lvalues and modifiable lvalues. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1722 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser: support for attributes over struct and union.xleroy2011-05-121-2/+4
| | | | | | | | cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of GCC attributes. Preliminary, untested support for ↵xleroy2011-04-141-0/+3
| | | | | | __aligned__ attribute git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵xleroy2010-09-011-0/+7
| | | | | | reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+6
| | | | | | | | | | | | | | | | | | | | | | - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-091-0/+5
| | | | | | | | Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites. Code cleanup: introduced Cutil.composite_info_{def,decl} git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1312 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-0/+169
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 14:42:49 +0000