aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Release 3.0 here we comev3.0Xavier Leroy2017-02-102-2/+3
|
* OS X: emit jumptables in .text segment, not .const segmentXavier Leroy2017-02-101-1/+1
| | | | | | 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.
* Use Printf.sprintf instead of Format.sprintf when possibleXavier Leroy2017-02-091-4/+4
| | | | Minor performance tweak. Printf is more efficient for plain formats involving no boxes.
* More tweaking of module 'open'Xavier Leroy2017-02-091-8/+10
| | | | I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-02-081-0/+7
|\
| * Changelog update concerning attribute handlingXavier Leroy2017-02-071-0/+7
| |
* | Revert broken change to Cutil.Bernhard Schommer2017-02-083-10/+10
|/ | | | | | 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 'master' of ssh://github.com/AbsInt/CompCertXavier Leroy2017-02-063-83/+36
|\
| * Simplified DebugInformation interface.Bernhard Schommer2017-02-063-83/+36
| | | | | | | | | | Instead of exporting and setting all functions we just fill the struct already in DebugInformation with the correct functions.
* | Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-0611-47/+148
|\ \ | |/ |/|
| * Preliminary support for the "noreturn" attributeXavier Leroy2017-02-062-12/+17
| | | | | | | | | | - 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.
| * Refactor the classification of attributesXavier Leroy2017-02-037-23/+101
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Use C99 syntax to print attributes over array typesXavier Leroy2017-02-011-4/+5
| | | | | | | | 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".
| * Regression: type attributes and array modifiersXavier Leroy2017-02-011-2/+4
| | | | | | | | | | | | | | Owing to the peculiarities of array types in Cutil.change_attributes_type, type-related attributes of the array element type were duplicated on the array type. E.g. elaborating 'const int a[10][5]' produced "a is an array of 5 const arrays of 10 const ints" instead of "a is an array of 5 arrays of 10 const ints"
| * Revised elaboration of attributesXavier Leroy2017-01-318-22/+38
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Cleanup opensBernhard Schommer2017-02-061-69/+62
| |
* | Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
| |
* | Removed shadowing openBernhard Schommer2017-02-061-5/+5
| |
* | Remove shadowing openBernhard Schommer2017-02-061-1/+1
| |
* | Remove unused open.Bernhard Schommer2017-02-061-1/+0
| |
* | Cleanup opens.Bernhard Schommer2017-02-061-9/+8
| | | | | | | | | | | | The Printf is only needed for the identifier functions. Furthermore the new intconst from Cutil is used to generate the integer constant and shadowing of the open C is removed.
* | Generalized function to allow adding hex strings.Bernhard Schommer2017-02-062-4/+8
| | | | | | | | | | The intconst function comes with an optional parameter to add an hex string for later printing.
* | Removed shadowing problems.Bernhard Schommer2017-02-061-9/+9
| | | | | | | | The clashing identifiers are now referenced explicitly.
* | Inlined open of ASTBernhard Schommer2017-02-061-7/+6
| |
* | Inlined open of ErrorsBernhard Schommer2017-02-061-10/+9
| |
* | Datatypes no longer shadows fst and sndBernhard Schommer2017-02-061-1/+1
| |
* | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
| | | | | | | | | | Locations are only used in two functions and can be referenced there directly.
* | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
| | | | | | | | The Locations are only used in one function.
* | Remove open AST.Bernhard Schommer2017-02-061-4/+3
| | | | | | | | The two types needed from AST are prefixed directly.
* | Remove unused openBernhard Schommer2017-02-061-1/+0
| |
* | Remove unused openBernhard Schommer2017-02-061-1/+0
| |
* | Inline fst and snd from Datatypes.Bernhard Schommer2017-02-061-0/+4
| | | | | | | | | | This avoids nameclashes with the Pervasives version of these functions.
* | Removed the open AST.Bernhard Schommer2017-02-062-10/+8
| | | | | | | | | | Only two types from AST are needed and the global shadowing open can be removed.
* | Remove unused open.Bernhard Schommer2017-02-061-1/+0
| |
* | Inline open Datatypes.Bernhard Schommer2017-02-061-3/+2
| |
* | Remove overriding open in Interp.Bernhard Schommer2017-02-031-11/+11
| |
* | Remove all overriding opens in Elab.ml. Bug 19872Bernhard Schommer2017-02-031-2/+2
| |
* | Removed Cabshelper open and avoided shadowing.Bernhard Schommer2017-02-032-8/+7
| | | | | | | | | | | | | | | | The Cabshelper is only used in 4 places, so we don't need a global open. Furhtermore the String.t type is now inlined for Cabs to avoid shadowing problems in Elab.ml Bug 19872
* | Remove unused opens.Bernhard Schommer2017-02-031-32/+28
| | | | | | | | | | | | Format was only used in one place without explicit module prefix. The same holds for Env. Bug 19872
* | Removed no longer working check.Bernhard Schommer2017-02-031-14/+4
| | | | | | | | | | | | Since anonymous struct members are kept in the fieldlist, the fieldlist can never be empty in this case. Bug 19872
* | Updated handcrafted.messages for __builtin_offsetofBernhard Schommer2017-02-011-753/+858
| |
* | Change the syntax to gcc/clangs syntax.Bernhard Schommer2017-02-013-4/+7
| | | | | | | | | | | | This only means that there must be one identifier at the begining and then a designator. Bug 20765
* | Merge pull request #159 from AbsInt/builtin_offsetofXavier Leroy2017-02-018-3/+73
|\ \ | | | | | | Implement offsetof via builtin
| * | Avoid overflows and report an error.Bernhard Schommer2017-01-312-7/+10
| | | | | | | | | | | | | | | | | | | | | 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
| * | Normalize offset to size_t kind.Bernhard Schommer2017-01-311-2/+4
| | |
| * | Remove superfluous check.Bernhard Schommer2017-01-311-7/+4
| | | | | | | | | | | | | | | | | | Gcc and clang do not raise an error for this, also it should work for the last array element which can be without size. Bug 20765
| * | Improve indentation.Bernhard Schommer2017-01-311-1/+1
| | |
| * | Remove blank lines.Bernhard Schommer2017-01-311-2/+0
| | |
| * | New version to support designators.Bernhard Schommer2017-01-248-22/+46
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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-202-43/+26
| | | | | | | | | | | | | | | | | | | | | | | | 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