aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Accept empty enum declaration after nonempty enum definition (#87)Bernhard Schommer2018-04-221-1/+1
| | | | Forward declarations of enums are not allowed in C99, however it is possible to have an empty enum declaration after the enum was defined.
* Better check for incomplete types in pointer subtraction (#92)Bernhard Schommer2018-04-201-0/+1
| | | | | | In the case of pointer subtraction both side can be pointers, for example if the difference between two array cells is calculated, so we need to check that both sides have complete types. Bug 23312
* Function defintions: keep the attributes from previous declarations (#89)Bernhard Schommer2018-04-191-1/+3
| | | | | | | | | | | | After calling enter_or_refine for a function identifier we need to keep the combined attributes. Here is an example where it makes a difference: ``` _Noreturn void f(int x); void f(int x) { } ``` Before this commit, the `_Noreturn` on the declaration is ignored when checking the definition. Bug 23385
* Revert "preserve static initialized variables (#81)"Xavier Leroy2018-04-101-9/+2
| | | | | | This part of PR#81 causes problems with long double static variables in math.h. Revert to the old behavior of not including static variables unless actually referenced.
* Check for redefinition of globals and preserve static initialized variables ↵Bernhard Schommer2018-04-092-6/+33
| | | | | | | | | | | | | | | | | (#81) * Added check for redefinition of globals. Since Cleanup may remove duplicated static functions or global definitions we need to check for duplication during elaboration, not just in C2C. Bug 23410 * Do not eliminate unreferenced static variables with initializers This way all initialized variables make it to the C2C pass, where the initializers are checked for constant-ness. Bug 23410
* Reject illegal initializations of aggregates at top-level (#79)Xavier Leroy2018-04-061-1/+10
| | | | | | | Examples such as the following were accepted but are invalid ISO C: char c[4] = 42; struct S { int x, y; } = 42; This commit rejects such initializations at top-level. Bug 23372
* 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
* Turn delicate case of designated re-initialization into error (#70)Xavier Leroy2018-03-301-37/+56
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* 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
* 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
* 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.
* Improve error messages.Bernhard Schommer2018-03-072-0/+6
| | | | | | | | 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
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-066-3/+24
| | | | | | | | | | | | | | | | | | 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.
* Struct return on OpenBSD now testedMichael Schmidt2018-02-191-1/+1
|
* Renamed StructReturn to structPassingBernhard Schommer2018-02-163-1/+1
|
* Move struct passing/return style to Machine.Bernhard Schommer2018-02-163-17/+72
| | | | | | Since the used configuration for passing and returning values struct values is pretty much static it can be hardwired into the machine settings.
* Added error summary in case of fatal error.Bernhard Schommer2018-02-092-0/+13
|
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-0813-34/+43
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-042-0/+13
| | | | | This time with the correct place for setting the destination files. Bug 20521
* Do not pass the env back from for stmt decls. (#42)Bernhard Schommer2017-12-121-7/+7
| | | | | | * Do not pass the env back from for stmt decls. This is the source of issue #211, the environment from the elaboration of the declaration and expressions in the for loop should not be passed back.
* Remove unused code. BUg 22642Bernhard Schommer2017-12-081-1/+0
|
* Store the different inlining cases.Bernhard Schommer2017-12-081-1/+1
| | | | | | | In order to correctly support the noinline attribute we must store whether the function was specified with an inline specifer, had a noinline attribute or nothing. Bug 22642
* Check recursively for const for modifiable lvalues (#32)Bernhard Schommer2017-10-171-2/+15
| | | | | | | | | | | | | | Check recursively for const for modifiable lvalues According to 6.3.2.1 a modifiable lvalue is an lvalue that does have a const-qualified type, and if it is a union or structure it does not have any member, including any member of all contained strutures or union, with a const-qualified type. The new check for modifiable lvalue additionally checks this now instead of only testing for toplevel const. Bug 22420
* Remove coq warnings (#28)Bernhard Schommer2017-09-222-20/+20
| | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* Issue P #25: make sure sizeof(long double) = sizeof(double) in all contexts.Xavier Leroy2017-08-221-10/+9
|
* Alphabet.v compiles even without the hints of BigNumPreludePierre Letouzey2017-06-061-1/+1
| | | | | | | | BigNumPrelude will soon leave Coq stdlib with the rest of the bignum library (apart from Int31 files) to become a separate package. With this (very minor) patch, Compcert compiles with or without the hints declared in BigNumPrelude.
* Make redefinition of composite a fatal error.Bernhard Schommer2017-05-091-2/+1
| | | | | | | The redefinition of a composite with a different tag type is now a fatal error. This should avoid problems when the composite is used. Bug 21542
* RISC-V port and assorted changesXavier Leroy2017-04-282-0/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Added handling if s.sloc <> s1.slocBernhard Schommer2017-03-241-2/+6
| | | | | | If the label is on a different line than the code we can still emit a line directive for the label. Bug 21232
* Emit line stmt after labels in general. Bug 21232Bernhard Schommer2017-03-241-10/+6
|
* Do not emit line info before case stmt.Bernhard Schommer2017-03-241-4/+9
| | | | | | | Since before a case statement is potentially unreachable code due to break, etc. it is better to skip printing line information directly before the case statement and print it afterwards. Bug 21232
* Added check for large arrays.Bernhard Schommer2017-02-213-0/+14
| | | | | | | 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 gcc noinline attribute.Bernhard Schommer2017-02-191-0/+1
| | | | The noinline attribute prevents functions from inlining.
* Added unused attribute and simplified checks.Bernhard Schommer2017-02-171-43/+82
| | | | | | | | | The attribute unused can be used to indicate if a variable or parameter is unused and no warning should be emitted for it. Furthermore this commit simplifies the check by adding a generic function to traverse the program. Bug 19872
* Adopted unused variable and attribtue checkBernhard Schommer2017-02-173-31/+55
| | | | | | | | | The unused variable check now uses two passes. One to collect the used variables and one to report the unused variables. Futhermore attribute checks are extended to composite declaration. Also the check is now performed after elaboration. Bug 19872
* Extended unused vars check for params.Bernhard Schommer2017-02-173-2/+9
| | | | | | The test now also checks whether the parameter are used at all in the function body. Bug 19872
* Added a simple check for unused variables.Bernhard Schommer2017-02-175-2/+88
| | | | | | | | | | | | | | | | | The check test whether the identifier is used at all in the function and if not issue a warning. It is not tested whether the usage is reachable at all, so int i; if (0) i; would not generate a warning. This is the same as gcc/clang does. The warning is disabled per default, but is active if -Wall is given. Bug 19872
* Checks can be applied add several places.Bernhard Schommer2017-02-173-8/+5
| | | | | | There should not be a single check place, since for example unknonw attributes should be check after elaboration and other simplifications.
* Also check the locals. Bug 19872.Bernhard Schommer2017-02-171-3/+7
|
* Added new module for checks on elaborated C codeBernhard Schommer2017-02-173-2/+114
| | | | | | | The new module adds a function which is called during parse after all C transformation have taken place for adding additional checks. Currently only unknown attribute are checked. Bug 19872
generated by cgit (git 2.34.1) at 2024-07-01 15:55:29 +0000