aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Add target ELFCyril SIX2021-06-012-0/+3
|
* Merge remote-tracking branch 'absint/master' into kvx-workCyril SIX2021-06-011-1/+1
|\
| * Support `# 0 ...` preprocessed line directiveXavier Leroy2021-06-011-1/+1
| | | | | | | | | | | | | | Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0848-192/+240
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
| * Fix evaluation order in emulation of bitfield assignmentXavier Leroy2021-05-021-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A bitfield assignment `x.b = f()` is expanded into a read-modify-write on `x.carrier`. Wrong results can occur if `x.carrier` is read before the call to `f()`, and `f` itself modifies a bitfield with the same carrier `x.carrier`. In this temporary fix, we play on the evaluation order implemented by the SimplExpr pass of CompCert (left-to-right for side-effecting subexpression) to make sure the read part of the read-modify-write sequence occurs after the evaluation of the right-hand side. More substantial fixes will be considered later. Fixes: #395
| * Support __builtin_unreachableXavier Leroy2021-05-021-1/+5
| | | | | | | | Not yet used for optimizations.
| * Fix spurious error on initialization of struct with flexible array memberXavier Leroy2021-05-021-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | The following is correct but was causing a "wrong type for array initializer" fatal error. ``` struct s { int n; int d[]; }; void f(void) { struct s x = {0}; } ``` Co-authored-by: Michael Schmidt <github@mschmidt.me>
| * Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-191-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | When desugaring a bitfield, allow any integral type that is 32 bits or smaller. Previously this was checking the rank of the type rather than the size. This rank check caused issues with standard headers that declare `uint32_t` to be an `unsigned long` rather than an `unsigned int`. Here, any bitfields declared as `uint32_t` were failing to compile even though they are still actually 32 bits. Co-authored-by: Amos Robinson <amos@gh.st>
| * Refactor cparser/Parse.mlXavier Leroy2021-04-191-31/+29
| | | | | | | | | | | | | | | | | | - Use pipeline notation `|>` for legibility and better GC behavior (in bytecode at least). - Introduce auxiliary functions. - Remove useless function parameters. - Fix the timing of the "Emulations" pass (because of an extra parameter, what was timed took zero time).
| * Ensure compatibility with future versions of MenhirLibXavier Leroy2021-04-191-6/+7
| | | | | | | | | | | | | | | | After Menhir version 20210310, the `Fail_pr` constructor of the `parse_result` type becomes `Fail_pr_full` with two extra arguments. This PR enables CompCert to handle both versions of the `parse_result` type in MenhirLib.
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-012-3/+12
|\ \
| * | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-132-3/+12
| | |
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-0148-226/+280
| | | | | | | | | | | | cfrontend/C2C.ml
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-234-5/+13
|\ \ \ | |/ / |/| / | |/ | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * "macosx" is now called "macos"Xavier Leroy2021-01-182-3/+3
| | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
| * Change warning for pragmas inside functionsXavier Leroy2021-01-161-1/+1
| | | | | | | | | | | | | | Follow-up to 35e2b11db. Put the warning "pragmas are ignored inside functions" inside the Unnamed category, so that it is displayed by default and cannot be disabled.
| * Ignore and warn about pragmas inside functionsXavier Leroy2021-01-071-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Pragmas can occur either outside external declarations, at the top level of a compilation unit, or within a compound statement, inside a function definition. The parse tree in cparse/C.mli cannot represent pragmas occuring within a compound statement. In this case, the elaborator used to silently move the pragma to top level, just before the function definition where the pragma occurs. It looks safer to just ignore pragmas occurring inside a function definition, and emit a specific warning.
| * AArch64: macOS portXavier Leroy2020-12-262-0/+4
| | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
| * C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
| | | | | | | | | | All the built-in types declared in $ARCH/CBuiltins.ml are now recognized as type names initially.
* | Turning loads into non-trapping when necessaryCyril SIX2020-12-152-1/+9
| |
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-1817-1119/+1319
|\|
| * Check ptr arithmetic for ++ and --Bernhard Schommer2020-09-201-10/+16
| | | | | | | | | | Also: improve check for ptr - integer. (Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
| * Add new static-assert token for deLexer utility; bug 29273Michael Schmidt2020-08-041-0/+1
| |
| * Add comments we missed to sync to GitHubChristoph Cullmann2020-07-301-0/+2
| |
| * Allow string_literals_list in _Static_assert.Bernhard Schommer2020-07-272-24/+25
| | | | | | | | | | | | Not all pre-processors concatenate string literal lists, however they are allowed in _Static_assert. This is similar to the rules for inline assembly etc.
| * More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-6/+10
| | | | | | | | We check that this builtin function is only called from within a variadic function and has the correct number of arguments.
| * cparser/handcrafted.messages: missing blank lineXavier Leroy2020-07-211-0/+1
| |
| * Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
| | | | | | | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'.
| * Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
| |
| * Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
| | | | | | | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366
| * Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
| |
| * Added error for redefined builtin.Bernhard Schommer2020-07-203-0/+6
| | | | | | | | | | | | We check in the initial environment if a function is already defined to avoid redefinition of functions that are part of the builtin environment.
| * Introduce additional "branch" build information.Bernhard Schommer2020-07-081-5/+5
| |
| * Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
| * Use library function.Bernhard Schommer2020-06-281-4/+1
| | | | | | | | | | | | | | The function String.uppercase was deprecated and the replacement function String.upercase_ascii was only available from OCaml 4.03.0. Since the minimal OCaml version is now 4.05.0 we can use the function String.upercase_ascii.
| * Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-2/+1
| | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
| * Check for errors after each pass.Bernhard Schommer2020-04-201-1/+8
| |
| * Added warning for packed composite with bitfields.Bernhard Schommer2020-04-201-0/+2
| |
| * Add location to transform functions.Bernhard Schommer2020-04-204-28/+28
| |
* | k1c -> kvx changesDavid Monniaux2020-05-262-3/+3
| |
* | 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
| | |
generated by cgit (git 2.34.1) at 2024-07-04 01:57:05 +0000