aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
...
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-081-3/+4
|\ \
| * | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-261-2/+2
| |\|
| | * Include typedef name in error message (#228)Bernhard Schommer2020-03-041-2/+2
| | | | | | | | | In case of redefinition of a typedef name with a different type.
| * | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-033-1/+47
| |\ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | The type of a wide char constant is wchar_t. (#223)Bernhard Schommer2020-02-241-1/+2
| | | | | | | | | | | | See ISO C2011 standard, section 6.4.4.4 para 11.
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-252-2/+2
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-242-2/+2
| |\| | | | |/ | |/| | | | mppa-work-upstream-merge
| | * Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-1/+1
| | | | | | | | | | | | | | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
| | * Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
| | | | | | | | | | | | Some preprocessors don't remove the vertical tab from the input so we should be able to handle them in the lexer.
* | | it now works, no more ugly hack to access thread local dataDavid Monniaux2020-02-241-1/+1
| | |
* | | seems to process _Thread_local but not till backendDavid Monniaux2020-02-243-3/+7
| | |
* | | actually process the modifiersDavid Monniaux2020-02-241-2/+12
| | |
* | | begin implementing thread_local storageDavid Monniaux2020-02-245-6/+31
| | |
* | | parse _Thread_localDavid Monniaux2020-02-246-3/+11
|/ /
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-1/+6
|\|
| * Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | | | | | | | | | | | | | | | | | Previously, using an unknown builtin function was treated like any other call to an undeclared function: a warning was emitted, and an error occurred at link-time. With this commit, using an unknown builtin function is an error, like in Clang.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-12-091-118/+42
|\| | | | | | | mppa-work-upstream-merge
| * Added back unused_ais_parameter warning.Bernhard Schommer2019-11-261-0/+1
| |
| * Simplified diagnostics module.Bernhard Schommer2019-11-251-118/+41
| | | | | | | | | | | | | | Instead of constructing four different lists for maintaining the state of the warnings only one list is now used. This list contains the name of the warning and a boolean indicating whether this option should be active by default. The rest is computed from this list.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-134-12/+36
|\| | | | | | | mppa-work-upstream-merge
| * Remove duplicated ticks.Bernhard Schommer2019-10-011-2/+2
| |
| * Use pointer type for evaluated constants.Bernhard Schommer2019-10-011-1/+1
| |
| * Various improvements for diagnostics.Bernhard Schommer2019-09-303-10/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Extend check for incomplete type. Extended the check to also include a check for variables with incomplete object type that are not arrays, that have an initializer. Furthermore the warning includes the type and variable name. * Warning for incomplete type in compound literals. Incomplete types are not allowed for compound literals, except for array types. * Extend type printing function. The type of a typedeof of an anonymous type should not be printed. Furthermore added '<anonymous>' to the printing of anonymous types. * Unify incomplete type errors message. The incomplete type error messages should all look the same including name of the variable, parameter, etc. and then the incomplete type.
| * Functions that are extern should stay extern (#201)Bernhard Schommer2019-09-251-1/+1
| | | | | | | | | | | | In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier). Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
* | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-0/+6
|\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * AArch64 portXavier Leroy2019-08-082-0/+6
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | Fix for test/regression/struct2.cCyril SIX2019-10-141-1/+2
| |
* | Tackling struct passing by value for the future K1C ABICyril SIX2019-10-143-2/+12
| |
* | Explicitly naming SP_split_args for easier greppingCyril SIX2019-10-141-1/+1
| |
* | __builtin_bswap16, 32 and 64Cyril SIX2019-09-201-1/+1
| |
* | Fixing machine description (error in wchar signedness + trying different ↵Cyril SIX2019-09-191-5/+32
| | | | | | | | value for passing structs)
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-1935-3830/+846
|\| | | | | | | mppa-work-upstream-merge
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+36
| | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-1712-87/+62
| | | | | | | | | | | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
| * Change condition for warning of conditional exprBernhard Schommer2019-07-101-1/+1
| | | | | | | | | | | | The warning should only be active if the optimization is active, so the check is only performed when the warning is active and additionally the command line flag -Obranchless is specified.
| * Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-0519-3635/+472
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
| * Deref is not safe.Bernhard Schommer2019-07-041-1/+1
| |
| * Added new diagnostic for non-linear conditionalsBernhard Schommer2019-07-046-1/+179
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The new diagnostics is triggered if a conditional is used that may not be transformed into linear code by the later by the if conversion. The new diagnostic is emitted if a conditional may contain an unsafe expression or is contained within another conditional, logical and or logical or expression. An expression is unsafe if it contains a call, changes memory or if its evaluation leads to undefined behavior, for example division and modulo. Also fixes a small typo in a comment in Cutil.
| * Added helper function for array types.Bernhard Schommer2019-07-042-0/+7
| | | | | | | | | | The function determines whether the given type is an array type or not.
| * Added statement traversal functions.Bernhard Schommer2019-07-041-107/+90
| | | | | | | | | | | | Refactored the checks functions by using higher order traversal functions for statements. Also introduce helper functions for the traversal of initializers.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-061-3/+5
|\|
| * New additional check for void parameters. (#174)Bernhard Schommer2019-06-031-3/+5
| | | | | | | | There should only be one unnamed parameter of type void in the parameter list.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-037-208/+229
|\| | | | | | | mppa-if-conversion
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-315-9/+9
| | | | | | | | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
| * Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
| | | | | | | | | | | | The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion.
| * Reworked elaboration of declarations/definitions.Bernhard Schommer2019-05-101-140/+138
| | | | | | | | | | | | | | | | | | | | | | | | Since a definition/declaration is completed with after the separator to the next init group member it is also possible to use it for example in the next init group member: char s[]="miaou", buf[sizeof s]; In order to ensure that this works the declarations are added to the environment directly during the elaboration of the init member group instead of later.
| * Change to AbsInt version string.Bernhard Schommer2019-05-101-1/+1
| | | | | | | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
| * Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
| | | | | | | | | | | | `_Complex` and `_Imaginary` are reserved keywords. Since CompCert does not support these types they could be used as identifiers. However the standard requires to reject this.
| * Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
| | | | | | | | | | | | | | | | | | Pass the environment to all expr eval functions since the functions themselve may be called recursively and modify the environment. The other change introduces new scopes that are strict subsets of their surrounding scopes for if, switch, while, do and for statement, as prescribed by ISO C standards.
generated by cgit (git 2.34.1) at 2024-05-20 01:13:46 +0000