aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | Use open_in_bin instead of open_in.Bernhard Schommer2022-11-051-1/+1
| | | | | | | | | | | | | | On platforms that do distinguish between text mode and binary mode, seek_in cannot reliably be used on files opened in text mode (open_in). The input file must therefore be opened in binary mode (open_in_bin). Bug 34075
* | Merge pull request #458 from AbsInt/simpl-expr-destsXavier Leroy2022-10-246-99/+220
|\ \ | | | | | | SimplExpr: revised handling of nested conditional, `||`, `&&` expressions
| * | Add test for nested conditional, &&, || expressionsXavier Leroy2022-10-013-1/+55
| | |
| * | SimplExpr: revised handling of nested conditional, `||`, `&&` operatorsXavier Leroy2022-10-013-98/+165
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a `For_set` destination, a temporary can be reused only if it always used with the same type. Otherwise, typing of Cminor code fails later in the compilation pipeline. This commit implements temporary reuse if and only if the typing constraint is respected. - For `&&` and `||`, it avoids the possibility of wrong reuse (as reported in #453). - For nested conditional expressions, it improves a bit the generated code by reusing the temporary when possible. Fixes: #453
* / Use .data.rel.ro section for const data with relocatable inits on ELF ↵Xavier Leroy2022-10-244-4/+16
|/ | | | | | | | | | | | | targets (#457) Follow-up to ed89275cb. AArch64, ARM, RISC-V and x86 ELF targets are changed. PowerPC / ELF is unchanged because we use the EABI variant, which has no `.data.rel.ro` section as far as I can see in GCC's output. (The SVR4 variant has `.data.rel.ro` but does not have `.sdata2`, which CompCert uses.) Fixes: #454
* test/export: use the standard headers from ../../runtime/includeXavier Leroy2022-09-231-1/+1
| | | | Just like in the other test/ directories.
* No need to set -std=c99 on the GNU C preprocessor command lineXavier Leroy2022-09-231-12/+12
| | | | The correct -std option is now added by ccomp itself.
* Support the `-std=<standard>` option (#456)Xavier Leroy2022-09-233-4/+24
| | | | | | | | | | | | | | It has two effects: - With a GNU toolchain, it's passed down to the preprocessor. This influences the contents of standard includes. - It determines the default effect of the "C11 feature" warning: -std=c99: warn on the use of C11 features -std=c11 or -std=c18: don't warn For backward compatiblity, the default, if no `-std` option is given, is to not warn, but to pass `-std=c99` to the preprocessor. Co-authored-by: Bernhard Schommer <bschommer@users.noreply.github.com>
* Add `Commandline.longopt` function for options of the form `-<key>=<arg>`Xavier Leroy2022-09-232-20/+18
| | | | | Also: use `int_of_string_opt` instead of `int_of_string` for slightly cleaner code.
* Improved help messages for the -g<n> and -gdwarf-<n> optionsXavier Leroy2022-09-231-3/+5
|
* Export the functions that control warningsXavier Leroy2022-09-231-0/+13
| | | | | Activation and deactivation of a given warning, plus set-as-error and remove-as-error.
* Temporary: don't run the regression/stringlit and regression/charlit testsXavier Leroy2022-09-191-1/+3
| | | | | Some versions of the glibc standard header `<uchar.h>` are not compatible with CompCert, causing the tests to fail on our CI.
* Support C11 Unicode string literals and character constants (#452)Xavier Leroy2022-09-1919-214/+490
| | | | | | | | | | | | | | | | | * Support C11 Unicode string literals and character constants * Add tests for C11 string literals and character constants * Better error message for ill-formed universal character names E.g. \u followed by fewer than 4 hex digits, or \U followed by fewer than 8 hex digits. * Add new warning `invalid-utf8` for byte sequences that are not valid UTF8. The warning is activated but not fatal by default. * Warn on uses of C11 Unicode character constants and string literals This uses the `c11-extensions` warning, which is off by default. * Support preprocessing option -finput-charset= for GNU toolchains
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-1919-7/+31
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* RTLgen: use the state and error monad for reserve_labels (#371)Pierre Nigron2022-09-194-24/+24
|
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-085-7/+7
| | | | | | Improves robustness in case of stronger (e)auto. This is in preparation of a change in Coq that will make auto and eauto stronger (https://github.com/coq/coq/pull/16293).
* Recognize more if-then-else statements that can be if-convertedXavier Leroy2022-09-052-126/+138
| | | | | | | | Ignore debug statements that could have prevented the recognition of a simple assignment. Since debug statements can formally get stuck, revise the simulation diagram to use the "eventually" modality.
* Introducing the "eventually" closure and new simulation diagrams using itXavier Leroy2022-09-051-27/+229
| | | | | | These diagrams enable the source program to make a number of finite transitions before eventually reaching a state that restores the simulation relation.
* `_Generic` is a C11 feature, should trigger the corresponding warning if activeXavier Leroy2022-09-041-0/+1
|
* Remove unused functions.Bernhard Schommer2022-09-031-7/+0
| | | | | | | | | | The `reset_constants` was only used for ARM and there it was superfluous since the jumptables, which it additionally resets in contrast to `reset_literals`, are always empty since jumptables are handled directly in during printing of the instruction. The `exists_constants` function is now also unused since we test directly for the different sizes in `emit_constants`.
* More simplifications for literal printingBernhard Schommer2022-09-036-31/+16
| | | | | | | Use the same code to split 64 bit literals into two 32 bit halfs as is used for 64 bit initialization data and print them in PrintAsm. This removes the need for a target specific printing function for 64 bit literals.
* Refactor emitting of constants.Bernhard Schommer2022-09-037-76/+21
| | | | | | The function was the same for nearly all backends and also the way 32 bit literals are printed so we moved it to PrintAsm. The 64 bit literals however are still target specific.
* Add `iter_literal*` functions with guaranteed iteration orderXavier Leroy2022-09-031-0/+12
| | | | This makes compilation runs more reproducible.
* Rework of struct member offsets for debug info.Bernhard Schommer2022-09-036-41/+92
| | | | | | | | | | | | | The struct member byte and bit offsets are now set based upon the new function `struct_layout` from Ctypes.v, thus using the same code to compute as used to generate the actual struct access. The struct offset member information is addded using the types computed after the translation in C2C. Therefore we need to store the new internal names of the members as well as the composites and use them when adding the offset information. Fixes: #445
* Introduce `struct_layout` functionBernhard Schommer2022-09-032-1/+28
| | | | | The `struct_layout` function computes for each member, that is neither padding nor zero-length, the same result as `field_offset`.
* Support mergeable sections for string literals and wide string literalsXavier Leroy2022-08-291-6/+13
| | | | | Note that strings containing null characters (code 0) cannot be put in a mergeable section, as this will confuse the linker's merging criterion.
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-2911-123/+145
| | | | | | | | | | | | On platforms that support them (ELF, macOS), use mergeable sections (like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals. Works only if the LITERAL section is the default one. If the user provided their own LITERAL section, all literals are put in it regardless of their sizes. Support for mergeable string sections is introduced in this commit too but needs further changes in C2C.ml .
* configure: recognize riscv32 and riscv64 for RISC-V targets (#448)Brad Smith2022-08-291-2/+3
|
* Do not use `.rodata.cst8` for floating-point literalsXavier Leroy2022-08-152-2/+2
| | | | | | | FP literals can have size 4 or 8 bytes, and it's incorrect to put a 4-byte literal in a mergeable section of chunk size 8. Fixes: #447
* Check early that extraction did not run into unimplemented axiomsXavier Leroy2022-07-071-0/+5
| | | | | | | | This has been known to happen, e.g. when using Flocq 4.0. If we don't stop the build at this point, a `ccomp` executable is built that fails every time it is run. Closes: #438
* Update comment about `deprecated-hint-rewrite-without-locality` warningXavier Leroy2022-07-071-4/+0
| | | | Follow-up to 353669f8f
* In test/regression: Use `static inline` instead of `inline`Xavier Leroy2022-07-052-5/+5
| | | | Fixes: #441
* Re-enable `deprecated-hint-rewrite-without-locality` warningXavier Leroy2022-07-051-2/+1
| | | | No longer triggered since commit df076edfe.
* Add [#global] qualifier on Hint Rewrite (#439)Pierre-Marie Pédrot2022-07-052-0/+12
| | | Adapt w.r.t. coq/coq#16004.
* More updates for release 3.11Xavier Leroy2022-06-271-2/+2
|
* Updates for release 3.11Xavier Leroy2022-06-252-3/+6
|
* Extend the boolean_equality tactic (#429)Jerome Hugues2022-06-251-1/+15
| | | | | Handle constructors with 5, 6 and 7 arguments. Handle lists.
* Support Coq 8.15.2Xavier Leroy2022-06-252-3/+3
|
* Update comment re: compile_switch functionXavier Leroy2022-06-251-1/+1
| | | | Fixes: #435
* Expand "j_s symb" to "jump symb, x31" assembly pseudo-instructionXavier Leroy2022-06-244-5/+6
| | | | | | | | | | As suggested by Léo Gourdin in #437. The previous expansion as a plain "j" instruction fails when the jump offset is too large to be represented (issue #436). Fixes: #436 Closes: #437
* First Changelog update for next release 3.11Xavier Leroy2022-06-201-0/+38
|
* Harden the configure script against \r\n end of linesXavier Leroy2022-06-201-6/+6
| | | | Fixes: #434
* AArch64: make register X29 callee-saveXavier Leroy2022-05-306-34/+34
| | | | | | | | | CompCert doesn't maintain a frame pointer in X29. However, it must treat X29 as callee-save, so that CompCert-generated code can be called from code that uses X29 as frame pointer. This commit makes X29 callee-save. In places where X29 was used as a temporary, X15 or X14 is used instead.
* Improve control-flow analysis of "noreturn" function callsXavier Leroy2022-05-191-4/+18
| | | | | | | | - Honor "noreturn" attributes and _Noreturn declarations on calls to function pointers. - Don't crash if a function type is an unknown typedef. (This can happen with local typedefs.) Instead, conservatively assume this function can return.
* Simplify handling of file suffixes.Bernhard Schommer2022-05-184-30/+28
| | | | | | | Since we are sure that all files passed have a valid extension we can use the OCaml function Filename.remove_extension and don't need to pass the suffixes. Bug 33218
* Fix computing of output filenames.Bernhard Schommer2022-05-181-13/+15
| | | | | | | At some places the ".c" was hard coded as suffix for computing the output filenames. This lead to problems if for example `-S`or `-c` is used with preprocessed files. Bug 33196
* Revised warning for non-prototyped function declarationsXavier Leroy2022-05-131-17/+22
| | | | | | - Emit the warning even for functions without parameters `int f() {...}` - Show what the type is after prototyping - Refactor this part of `elab_fundef` slightly
* Some tests for _GenericXavier Leroy2022-05-133-1/+115
|
* Support _Generic from ISO C 2011Xavier Leroy2022-05-137-711/+1031
| | | | Entirely handled during elaboration. No impact on the verified part of CompCert.
* Fix the parsing of unprototyped function types in casts (#431)Xavier Leroy2022-05-091-2/+2
| | | | | Before, in casts, `int (*)()` was parsed like `int (*)(void)`. This caused expressions like `((int (*)()) &f)(42)` to be rejected. Declarations were correctly parsed.
generated by cgit (git 2.34.1) at 2024-05-09 19:29:35 +0000