aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-1821-49/+39
|
* fix modeling issue (Vundef for load outside of bounds)David Monniaux2021-06-161-2/+7
|
* Use qemu-6.0.0 for PPC as the 3.1.0 version shipping with the Debian in the ↵David Monniaux2021-06-121-2/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | docker has buggy float Squashed commit of the following: commit 54d1983cd8d8551c28109a506a752a971897f4ed Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:48:02 2021 +0200 sudo make install commit 49af5c63eff29a49f3cb466a6b6af44570d85352 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:43:17 2021 +0200 pixman commit d78ab98e5751dd3ae0299a3e8c271472ebd8bb63 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:36:30 2021 +0200 libglib commit 0808bf51be42b04c2db4ccc914633407c1309585 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:31:46 2021 +0200 don't show verbose untar commit 972c244c72d9a30fee41dc7cbcc3698a49b6cde6 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:30:32 2021 +0200 ninja-build commit a1c261d01abc1c62ea94d56cfc9cce90887db680 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:28:14 2021 +0200 install ninja commit 92990598283f624d598853851c3edb2650f45b4b Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:25:17 2021 +0200 untar commit a225a0dcea26dd8888be535aa1aec4a58007679d Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:20:32 2021 +0200 install wget first commit 3b2c30ab6a953bde9d09034d38c5919a9425163d Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:17:09 2021 +0200 install recent qemu
* show qemu versionDavid Monniaux2021-06-111-0/+1
|
* disable ppc partiallyDavid Monniaux2021-06-111-2/+6
|
* compile non yarpgen tests without -static; this should workDavid Monniaux2021-06-111-4/+4
|
* disable PPC64; can't link and don't know whyDavid Monniaux2021-06-111-2/+2
|
* fix bad pathsDavid Monniaux2021-06-111-2/+2
|
* don't use -static on ppcDavid Monniaux2021-06-111-4/+4
|
* path issuesDavid Monniaux2021-06-111-6/+6
|
* add PPC to CI and remove ugly hack for qemu linker pathsDavid Monniaux2021-06-111-56/+62
|
* Merge branch 'kvx-work' of ↵David Monniaux2021-06-111-39/+0
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * remove filter fileLéo Gourdin2021-06-101-39/+0
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into kvx-workDavid Monniaux2021-06-112-3/+13
|\ \ | |/ |/| | | fix for comments on x86-64 MacOS
| * x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-3/+11
| | | | | | | | | | | | | | | | | | As reported in #399, it seems better to use `##` instead of `#` as comment delimiter under macOS. For the time being we keep using `#` for Linux and Cygwin. Closes: #399
* | push afadl test exampleLéo Gourdin2021-06-092-0/+21
| |
* | Merge branch 'kvx-work' of ↵Olivier Lebeltel2021-06-091-1/+1
|\ \ | | | | | | | | | https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy/CompCert into kvx-work
| * | comment is now ## due to some weird MacOS bugDavid Monniaux2021-06-091-1/+1
| | |
* | | added config_macos_x86_64.shOlivier Lebeltel2021-06-091-0/+1
|/ /
* | MacOS compatibilityDavid Monniaux2021-06-091-1/+1
| |
* | run CI on kvx-work-ssa kvx-work-velusDavid Monniaux2021-06-081-49/+57
| |
* | omega -> liaDavid Monniaux2021-06-081-8/+8
| |
* | coq 8.13.2David Monniaux2021-06-071-2/+1
| |
* | divisionDavid Monniaux2021-06-072-3/+4
| |
* | timingDavid Monniaux2021-06-072-0/+117
| |
* | Merge branch 'kvx-work' of ↵David Monniaux2021-06-06340-6016/+11801
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * | Remove install path bricolage for kvxv3.9_kvxCyril SIX2021-06-012-4/+5
| | |
| * | Merge remote-tracking branch 'verimag/manuscript' into kvx-workCyril SIX2021-06-011-13/+11
| |\ \
| | * | Do not rotate if the CB was already at the end.Cyril SIX2021-04-281-1/+5
| | | |
| | * | Heuristic counter updateCyril SIX2021-04-281-12/+6
| | | |
| * | | Update INSTALL.mdCyril SIX2021-06-011-0/+6
| | | |
| * | | Fixing build for KVX (missing ccomp_kvx_fixes.h for runtime)Cyril SIX2021-06-011-0/+1
| | | |
| * | | Add target ELFCyril SIX2021-06-014-2/+7
| | | |
| * | | Merge remote-tracking branch 'absint/master' into kvx-workCyril SIX2021-06-013-4/+6
| |\ \ \ | | | |/ | | |/|
| | * | 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
| | * | Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
| | | | | | | | | | | | | | | | E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
| | * | Update for release 3.9Xavier Leroy2021-05-101-1/+1
| | | |
| | * | Update Changelog for release 3.9Xavier Leroy2021-05-091-0/+3
| | | |
| | * | Update for release 3.9Xavier Leroy2021-05-091-4/+5
| | | | | | | | | | | | | | | | Also: limit the max width of the page, to avoid very long lines.
| | * | Update ChangelogXavier Leroy2021-05-081-1/+11
| | | |
| | * | Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-08149-860/+1171
| | | | | | | | | | | | | | | | | | | | | | | | 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_expectXavier Leroy2021-05-021-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Not yet used for optimizations. Actually, __builtin_expect is removed during C2C conversion, otherwise the conversion to type "long" produces inefficient code on 64-bit platforms.
| | * | Support __builtin_unreachableXavier Leroy2021-05-028-2/+32
| | | | | | | | | | | | | | | | 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>
| | * | Update ChangelogXavier Leroy2021-04-291-0/+53
| | | |
| | * | Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Variables without init do not generated any assembly code so no entry in the json AST should be generated. They correspond to extern variables without initializer that are defined in another compilation unit. Bug 30112
| | * | MacOS: add a #define __DARWIN_OS_INLINEXavier Leroy2021-04-271-2/+2
| | | | | | | | | | | | | | | | | | | | Seems necessary for the standard headers of a recent version of XCode. The actual definition in the standard headers is only for GNUC.
| | * | Support Coq 8.13.2Xavier Leroy2021-04-271-2/+2
| | | |
| | * | More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Volatile load and store are expanded later and also use the ld/std instructions, therefore the same fixes that are applied as well for them. Bug 30983
generated by cgit (git 2.34.1) at 2024-07-01 05:23:53 +0000