aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Define C11 conditional feature macros (#77)Bernhard Schommer2018-04-061-1/+10
| | | | | | | | These macros can be defined to indicate that variable length arrays, the _Complex type, atomics and threads are not supported. Since the _Complex type is not supported, we also need to undefine __STDC_IEC_559_COMPLEX__ Bug 23408
* Allow declaration of composites in bitfield size.Bernhard Schommer2018-04-051-11/+20
| | | | | | It is allowed to define a composite within a bitfield size expression using for example sizeof. Bug 23360
* Error for subtraction arithmetic type - pointer type (#73)Bernhard Schommer2018-04-051-3/+0
| | | | | | Substraction is only allowed for pointer - pointer, pointer - arithmetic or arithmetic - arithmetic. This also leads to a retyping error later. Bug 23357
* Bug 23327Bernhard Schommer2018-04-030-0/+0
|
* Turn delicate case of designated re-initialization into error (#70)Xavier Leroy2018-03-303-38/+62
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Consider: struct P { int x, y; } struct S { struct P p; } struct P p0 = { 1,2 }; struct S s1 = { .p = p0; .p.x = 3 }; ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e. the initialization of s1.p.y to p0.y implied by ".p = p0" is kept, even though the initialization of s1.p.x to p0.x is overwritten by ".p.x = 3". GCC, old versions of Clang, and previous versions of CompCert initialize s1.p.y to the default value 0. I.e. the initialization ".p = p0" is forgotten, leaving default values for the fields of .p before ".p.x = 3" takes effect. Implementing the proper ISO C99 semantics in CompCert is difficult, owing to a mismatch between the intended semantics and the C.init representation of initializers. This commit turns the delicate case of reinitialization above (re-initializing a member of a composite that has already been initialized as a whole) into a compile-time error. We will then see if the delicate case occurs in practice and needs further attention.
* Reject casts to struct/union types (#68)Bernhard Schommer2018-03-291-3/+0
| | | | | | | | | | | The ISO C99 standard allows cast only if the type name involved is either a void type or a scalar type. For compatibility with GCC and Clang we used to support casting a struct or union to exactly the same struct or union type. That does not seem useful in practice and complicates conformance testing. This commit gets rid of this exception to the C99 rule. Bug 23310
* Don't overwrite initializer of anonymous union member. (#69)Bernhard Schommer2018-03-291-1/+1
| | | | | Instead of overwriting the initializer of the anonymous member we should just keep it. Bug 23353
* Fix 23332Bernhard Schommer2018-03-280-0/+0
|
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-285-17/+14
| | | | | | | Implicit Arguments is deprecated in Coq since 8.6 or so. Some Implicit Arguments remained in Flocq but were recently changed to Arguments. Apply the same change to our local copy of Flocq. As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
* Sizeof and _Alignof are not allowed on bit-fields (#67)Bernhard Schommer2018-03-273-1/+17
| | | | | | | Sizeof and _Alignof are not allowed on bit-fields Sizeof and _Alignof are not allowed to be applied to a expression that designates a bit-field member. Bug 23311
* Bug 23320Bernhard Schommer2018-03-270-0/+0
|
* Fix mistake in Bitfield transformation (#66)Michael Schmidt2018-03-271-2/+2
| | | Unions containing multiple bit fields were transformed incorrectly.
* Arrays should decay to pointers (#65)Bernhard Schommer2018-03-271-2/+3
| | | | | | | Arrays should decay to pointers except if they are used as operands of sizeof, _Alignof or as operand of the unary &. The "comma" sequencing operator was missing a "decay" on the type of its second argument. All other operators "decay" their operands correctly. Bug 23299 Bug 23311
* Improve error messages for anonymous bit-fields (#64)Bernhard Schommer2018-03-231-7/+10
| | | | | | If an anonymous bit-field member is declared wrong, i.e. a wrong type is used or a too large size is used the error message now prints <anonymous> instead of an empty string. Bug 23292
* Do not allow inline on main and warn for Noreturn (#63)Bernhard Schommer2018-03-231-0/+4
| | | | | | | | | | | | | | * Do not allow inline on main(). The C99 standard says that in a hosted environment inline shall not appear in a declaration of main. Bug 23274 * Added warning for _Noreturn on main(). The C11 standard does not allow any function specifier on the main function. Bug 23274
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
| | | | | | | This should avoid cluttering the assembler output with .ascii "\n" lines if the annotation ends with a string and make for a better readability. Bug 23169
* Anchor patterns to the top-level directory when appropriateXavier Leroy2018-03-131-47/+47
| | | | | | It's OK to ignore *.o in any directory, but it's safer to ignore "/ccomp" (ccomp in the top-level directory) than to ignore "ccomp" (ccomp in any directory).
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-133-3/+3
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
| | | | | | It seems necessary that the mulitplication for the high part of split registers is put into brackets. Bug 23169
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
| | | | | The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3. Fix 23199
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-122-5/+2
| | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
|
* StructPassing and annotations, continuedXavier Leroy2018-03-091-9/+7
| | | | | struct/union arguments to annotations should not be transformed at top level, but the regular function calls contained within must be transformed recursively.
* Do not transfer arguments for annotations.Bernhard Schommer2018-03-091-2/+5
| | | | | | | In order to ensure that no transformation for arguments to builtin annotations are used, the original unchanged arguments are used. Bug 23179
* Add explicit interface to cparser/pre_parser_aux.mlXavier Leroy2018-03-092-5/+28
| | | | | | | This should help with parallel builds, which currently fail sometimes owing to a lack of a dependency on pre_parser_aux.cmi. Also: move documentation comments from the .ml to the .mli
* StructPassing: do not transform arguments to annotation built-insXavier Leroy2018-03-091-2/+6
| | | | | | | | | | | | Make sure struct/union arguments to __builtin_annot and related builtins are always passed by reference using the default passing mode, regardless of the ABI for passing struct/unions to "real" functions. This ensures portability of annotations across ABIs, and avoids mismatches between the annotation text and the actual number of arguments (when a struct/union argument is passed as N integer arguments). A similar special case already existed for __builtin_va_arg.
* Do not use default printer for variable names.Bernhard Schommer2018-03-091-2/+8
| | | | | | Printing variable names with the default expression printer results in newlines in the outputed error message. Bug 23169
* Perform quoting for json.Bernhard Schommer2018-03-081-1/+8
| | | | | | The strings for json need quoting of special characters such as \" and \\. Bug 22438
* Print x2 for riscV stack pointer.Bernhard Schommer2018-03-081-2/+2
| | | | | | x2 is the stack pointer of the riscV, both sp and x2 are supported but to be safe use x2 in annotations. Bug 23176
* Update manpage for new warning name classMichael Schmidt2018-03-081-0/+4
|
* Print symbols as symbols.Bernhard Schommer2018-03-084-36/+61
| | | | | | This allows us to replacing them by their address in valex and additionally checking them. Bug 22438
* Fix register naming for stack pointer.Bernhard Schommer2018-03-083-5/+6
| | | | | | It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and 'sp' for riscV. Bug 23176.
* Removed % prefix from ais annot register names.Bernhard Schommer2018-03-081-1/+18
| | | | | Registers should not contain the % prefix for ais annotations. Bug 23176
* Improve error messages.Bernhard Schommer2018-03-073-16/+20
| | | | | | | | Include the format specifier in error message when available in order to make it easier to spot the broken ais parameter. Futhermore introduce a new warning for unused ais parameters. Bug 22464
* Reword error message. Fix 22464Bernhard Schommer2018-03-071-2/+2
|
* Also use binary output for arm. Fix 23172Bernhard Schommer2018-03-071-1/+1
|
* Improve wording.Bernhard Schommer2018-03-071-1/+1
| | | | | Mention that it is a global memory cell. Fix 22464
* Use binary output.Bernhard Schommer2018-03-071-1/+1
| | | | | | This should avoid problems when newlines are used in string constants etc. Bug 23172
* Improve and simplify error messages.Bernhard Schommer2018-03-073-36/+55
| | | | | | | | The checks on the argument and format arguments are now performed during C2C translation by calling the validate_ais_annotations function and result in an error instead of a warning in the backend to be more consistent with the rest of the builtin functions.
* Fix arm compile broken by merge problems.Bernhard Schommer2018-03-061-4/+2
|
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-0615-73/+289
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Removed no longer needed struct passing.Bernhard Schommer2018-02-261-2/+0
|
* Support Coq 8.7.2Xavier Leroy2018-02-191-3/+3
|
* Merge pull request #60 from AbsIntPrivate/struct-abi-internalXavier Leroy2018-02-199-110/+80
|\ | | | | Move the struct-return / struct-passing platform aspects from compcert.ini to cparser/Machine.ml
| * Struct return on OpenBSD now testedMichael Schmidt2018-02-191-1/+1
| |
| * Renamed StructReturn to structPassingBernhard Schommer2018-02-163-1/+1
| |
| * Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-163-89/+0
| |
| * Move struct passing/return style to Machine.Bernhard Schommer2018-02-164-18/+77
| | | | | | | | | | | | Since the used configuration for passing and returning values struct values is pretty much static it can be hardwired into the machine settings.
| * Rename abi for ppc-linux targets.Bernhard Schommer2018-02-161-2/+2
|/
* Fix typo in commentMichael Schmidt2018-02-161-1/+1
|
generated by cgit (git 2.34.1) at 2024-06-29 13:32:34 +0000