aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Import prim token notations before using themJason Gross2018-08-274-1/+4
| | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. Closes #246 Closes #250
* Bug 24351Bernhard Schommer2018-08-270-0/+0
|
* Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| | | | | | | For consistency with other generated .v files, and because it protects against editing the generated file, see Github issue #248. Closes: #248
* Improve execution of regression testsXavier Leroy2018-08-244-16/+45
| | | | | | - Make it possible to skip tests on some platforms - Make it possible to expect a failure (typically: of the reference interpreter) - Stop on error
* Edit documentation comments for [alignas_attribute] and [has_std_alignas]Xavier Leroy2018-08-241-2/+3
|
* More standard compliant handling of _Alignas.Bernhard Schommer2018-08-241-0/+11
| | | | | | | | | | | The C11 standard disallows the usage of _Alignas for: - Bit-field members of struct or union types - Typedefs - Function Defintions - Parameters of functions It is still allowed to use the gcc attribute for these constructs. Bug 23391
* Add check for _Alignas attribute.Bernhard Schommer2018-08-242-0/+6
| | | | | | The check tests whether the standard _Alignas is contained within a given attribute list. Bug 23391
* Reimplement attr_array_applicable in terms of class_of_attributeXavier Leroy2018-08-241-3/+2
| | | | | | | | | | | | | Since commit 5963ac4, "aligned" attributes and _Alignas qualifiers are represented differently, causing them to be treated differently by the previous implementation of Cutil.attr_array_applicable. This is incorrect and inconsistent with what happens during elaboration of array types in Elab. This PR reimplements attr_array_applicable in terms of class_of_attribute. Just like during elaboration, attributes of the Attr_type class are applied to the type of array elements, other attributes stay attached to the array type.
* Preserve attribute(("aligned")) in the AST, don't map it to _AlignasXavier Leroy2018-08-242-2/+3
| | | | | | | | | | | | | | We used to recognize attribute(("aligned"(N))) and map it to _Alignas(N) during elaboration. However, we want to restrict the places where _Alignas can occur, as standardized in ISO C11, while leaving more freedom for the placement of the "aligned" attribute. As a first step in this direction, this commit keeps the "aligned" attribute unchanged in the AST, and distinct from _Alignas attributes. Both attributes are honored when it comes to determining the actual alignment of a type.
* Fix typo in pattern match of error case, bug 24326Michael Schmidt2018-08-221-1/+1
|
* Document new named warning for tentative static definitions with incomplete ↵Michael Schmidt2018-08-211-0/+4
| | | | type, bug 23377
* Document new named warning for flexible arrays, bug 23324Michael Schmidt2018-08-211-1/+1
|
* Document new named warning for flexible arrays, bug 23324Michael Schmidt2018-08-211-0/+4
|
* Fix passing of -u to linker.Bernhard Schommer2018-08-211-1/+1
| | | | | | Instead of just passing -u to the linker also pass the value of the option to the linker. Bug 24316
* Diagnostic for wrong application of restrict (#119)Bernhard Schommer2018-08-213-7/+33
| | | | | | Restrict is only allowed for pointers whose referenced type is an object type or incomplete type, but not a function type. Bug 23397
* Harden the extasm.c test, continuedXavier Leroy2018-08-202-5/+5
| | | | | Follow-up to b9a6a50. clang is not happy with COMPCERT_MODEL=32sse2 ("bad suffix on integer"), so use MODEL_32sse2 and ARCH_x86 instead.
* Improve support and diagnostic for type qualified arrays (#118)Bernhard Schommer2018-08-203-1/+18
| | | | | | | | | | | | | | | | * Add diagnostic for type qualified arrays that occur in the wrong place Arrays with type qualifiers (e.g. int t[const 5]) are only allowed as function parameters and for them only the outermost array type derivation. Bug 23400 * Keep attributes from array for argument conversion Type qualifiers of arrays in function parameters are just syntactic sugar to allow adding them to the resulting pointer type. Hence, when a qualified array type such as `int t[const 5]` decays into a pointer type during argument conversion, the pointer type should be qualified, e.g. `int * const t`.
* Added warning for incomplete tentative static defs (#114)Bernhard Schommer2018-08-203-4/+11
| | | | | | Tentative static definitions with incomplete type are not allowed in C99. However most popular compilers support them and warn about them. Bug 23377
* Harden the extasm.c testXavier Leroy2018-08-202-2/+7
| | | | | | | Pass more info from CompCert's configuration as #define on command line. Use this info to improve the "64 bit" detection in extasm.c. (Before it fails with powerpc-ppc64, which has 64-bit int regs but couldn't be detected with #ifdefs.)
* Additional checks for flex arrays in structs (#93)Bernhard Schommer2018-08-205-5/+30
| | | | | | | | | | | | | | | * Error for structs with only flex array member Flexible array members are only allowed if another member exists. Bug 23324 * Added checks for nesting of structs with flex array members Warn if a struct with a flex array member is used as array element or member of another struct. Such usage is dubious. Bug 23324 Don't warn if the struct-with-flex-array is a member of an union.
* Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-204-5/+25
| | | | | | | | | | | | | Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
* Turn error into fatal error for unnamed parameter.Bernhard Schommer2018-08-201-2/+4
| | | | | | Since the parameter name gets used in other error messages it results in messages without names. Bug 24283
* For "packed" attribute, check that 3rd parameter is 0 or 1Xavier Leroy2018-08-171-1/+1
| | | | | | | It's meant as a Boolean (byte-swap or not), so any other value is dangerous. The error message is the generic "ill-formed 'packed' attribute". Maybe we don't need a custom error message.
* Wrong AST for GCC-style attributesXavier Leroy2018-08-171-1/+1
| | | | | The list of arguments to the attribute was missing a reverse, hence attribute(("foo"(1,2,3))) was actually read as attribute(("foo"(3,2,1))).
* Check for bit-fields in __builtin_offsetofXavier Leroy2018-08-171-1/+4
| | | | __builtin_offsetof(struct s, f) is an error if f is a bit-field.
* Issue with packed structs and sizeof, alignof, offsetof in cparser/Xavier Leroy2018-08-178-102/+202
| | | | | | | | | | | | | | | | | | | | | | | | | | | CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field): - the reference implementation, in Coq, from cfrontend/Ctypes.v - the implementation used during elaboration, in OCaml, from cparser/Cutil.ml The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used. This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example: ``` struct __packed__(1) s { char c; short s; int i; }; assert (__builtin_offsetof(struct s, i) == 3); assert (sizeof(struct s) = sizeof(char[sizeof(struct s)])); ``` The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs. This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout. Related changes: * cparser/Cutil: add `packing_parameters` function to extract packing info from attributes * cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout * cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.) * cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)). * cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab * cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/. * test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
* Added a check for parameters without identifiers. (#128)Bernhard Schommer2018-08-171-5/+7
| | | | | It is not allowed in C to have a parameter in a parameter list without an identifier. Bug 24283
* Earlier check for invalid asm outputs. (#130)Bernhard Schommer2018-08-172-2/+5
| | | | | | Since a non modifiable lvalue is an invalid asm output it should be checked earlier, otherwise this leads to a retyping error later. Bug 24285
* Also check parameters for unknown attributes.Bernhard Schommer2018-08-161-0/+1
| | | | | | Parameters also need to be checkd for unknown attributes, like all other declarations. Bug 24277
* Remove undocumented option.Bernhard Schommer2018-08-071-4/+0
| | | | | The option -doptions was never document and no longer works. Bug 19775
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-0213-99/+98
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Added Pldi to instr_size.Bernhard Schommer2018-08-011-0/+1
| | | | | | Since Pldi generates two instructions instr_size of Pldi should return 2. Bug 24218
* Bug 24150Michael Schmidt2018-07-190-0/+0
|
* Update cparser/GNUmakefile to be compatible with BSD's cut utility. Choose ↵Michael Schmidt2018-07-191-2/+2
| | | | better name for generated test cases.
* Compatibility with OCaml 4.07 (#241) continuedBernhard Schommer2018-07-121-1/+1
| | | | | | | Additionally an open !Integers is needed for the open Integers in the RISC-V Asmexpand, since Integers defines an Int64 module. This silences the warning 44 triggered. Bug 24090
* Fix expansion of ctzl/clzl builtin for 64bit targets (#127)Michael Schmidt2018-07-121-2/+15
| | | | bug 24105, issue #243: expand correct version of ctzl/clzl builtin when long type is 64bit wide
* Bug 24090, Bug 24091Bernhard Schommer2018-07-110-0/+0
|
* Compatibility with OCaml 4.07 (#241) continuedXavier Leroy2018-07-101-1/+1
| | | | | This is a follow-up to commit 6e1a5ce. Another `open! Floats` is needed.
* Clean .foo.aux files created by coqcXavier Leroy2018-07-101-1/+1
|
* Support Coq 8.8.1 (#242)Xavier Leroy2018-07-101-3/+3
|
* Compatibility with OCaml 4.07 (#241)Xavier Leroy2018-07-101-1/+1
| | | | | | | | | OCaml 4.07 introduces a Float submodule of the Stdlib opened-by-default compilation unit. CompCert's Float compilation unit also has a Float submodule. This triggers warning 44 when Floats is opened. The workaround is just to silence the warning with `open! Floats`. Closes: #241
* Update delexer for BUILTIN_OFFSETOF. Bug 23929Bernhard Schommer2018-07-051-0/+1
|
* Bug 23405Bernhard Schommer2018-06-250-0/+0
|
* Typo in -iquote preprocessing option (#239)Frédéric Besson2018-06-201-1/+1
| | | The `-iquote` option was passed to the GNU preprocessor as `-iquore`
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-202-4/+21
| | | | | Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info. Closes: #226.
* Bug 23926Bernhard Schommer2018-06-180-0/+0
|
* Typo in Ctyping entryXavier Leroy2018-06-171-1/+1
|
* Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-176-93/+145
| | | | | | | | | | | | | | | | | | | * Outgoing stack slots are set to Vundef on return from a function call, modeling the fact that the callee could write into those stack slots. (CompCert-generated code does not do this, but code generated by other compilers sometimes does.) * Adapt Stackingproof to this new semantics. This requires tighter reasoning on how Linear's locsets are related at call points and at return points. * Most of this reasoning was moved from Stackingproof to Lineartyping, because it can be expressed purely in terms of the Linear semantics, and tracked through the wt_state predicate. * Factor out and into Conventions.v: the notion of callee-save locations, the "agree_callee_save" predicate, and useful lemmas on Locmap.setpair. Now the same "agree_callee_save" predicate is used in Allocproof and in Stackingproof.
* Ignore *.v files generated by testsBernhard Schommer2018-06-071-0/+2
|
* Bug 23383Bernhard Schommer2018-06-070-0/+0
|
generated by cgit (git 2.34.1) at 2024-07-02 20:09:59 +0000