aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* 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
* Do not optimize away the 'return 0' at end of 'main'Xavier Leroy2017-02-171-7/+5
| | | | | | As a cosmetic optimization enabled by the static analysis in Cflow, we used to not insert a 'return 0' at end of 'main' if the body of 'main' cannot fall through. Since this optimization is cosmetic (the back-end will remove the 'return 0' if unused) and since we don't fully trust this static analysis, revert this optimization and always insert 'return 0'.
* Control-flow analysis: bug in switch without defaultXavier Leroy2017-02-171-1/+30
| | | | If no 'default' case appears in a 'switch', one is implicit at the end of the switch body, making possible to have a fall-through behavior.
* Added _exit.Bernhard Schommer2017-02-171-1/+1
|
* Add longjmp. Bug 21009Bernhard Schommer2017-02-171-1/+1
|
* Added handling for noreturn std functions.Bernhard Schommer2017-02-163-3/+14
| | | | | | | | | | The C11 standard declares exit,abort,_Exit,quick_exit and thrd_exit as _Noreturn however this is not included in older C libs and leads to false negatives in reporting _Noreturn and return type warnings. This can be avoided by enhancing the noreturn check of the Cflow analysis to also test if one of the above functions is called. Bug 21009
* Reverted changes in Cutil and catch in Cflow.Bernhard Schommer2017-02-162-17/+5
| | | | | | Instead of changing the definition of sizeof we now ignore errors raise in the Cflow module. Bug 21005
* Fixed problem with local structs/unions in Cflow.Bernhard Schommer2017-02-161-4/+17
| | | | | | | | Since the function environment does not necessary contain structs and unions defined in sizeof expressions the evaluation should be not constant and the Environment excpetions should be catched. Fix 21005
* Merge pull request #162 from AbsInt/return-analysis-2Xavier Leroy2017-02-155-32/+290
|\ | | | | | | Improved warnings related to function returns
| * Cflow: analysis of "switch" was too impreciseXavier Leroy2017-02-071-2/+3
| | | | | | | | Plus: updated comments.
| * Revised, more precise implementation of control-flow analysisXavier Leroy2017-02-071-48/+98
| | | | | | | | The new implementation keeps track of goto labels that are actually branched to. It is less optimized than the previous implementation (no bit vectors) but perhaps easier to read.
| * Control-flow analysis: wrong flow for "case"/"default" statementsXavier Leroy2017-02-071-4/+6
| | | | | | | | Those labeled statements can be entered either by fall-through or by the enclosing switch.
| * More precise warnings about function returnsXavier Leroy2017-02-075-32/+237
| | | | | | | | | | | | | | | | | | | | | | | | This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to - warn for non-void functions that can return by falling through the body - warn more precisely for _Noreturn functions that can return - introduce the "return 0" in "main" functions less often (cosmetic). For the control-flow analysis, the following conservative approximations are made: - any "goto" label is reachable - all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case) - the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants.
* | Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-5/+5
| | | | | | | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* | 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.
* | 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 'elaboration-of-attributes'Xavier Leroy2017-02-066-42/+129
|\
| * Preliminary support for the "noreturn" attributeXavier Leroy2017-02-061-11/+15
| | | | | | | | | | - 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-035-23/+87
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-314-17/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | 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.
* | Remove all overriding opens in Elab.ml. Bug 19872Bernhard Schommer2017-02-031-2/+2
| |
generated by cgit (git 2.34.1) at 2024-06-18 12:49:43 +0000