aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)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 d...David Monniaux2021-06-121-2/+5
* 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-06-111-39/+0
|\
| * 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
|\ \ | |/ |/|
| * x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-3/+11
* | push afadl test exampleLéo Gourdin2021-06-092-0/+21
* | Merge branch 'kvx-work' of https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy...Olivier Lebeltel2021-06-091-1/+1
|\ \
| * | 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-06-06340-6016/+11801
|\ \
| * | 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
| | * | Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
| | * | 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
| | * | Update ChangelogXavier Leroy2021-05-081-1/+11
| | * | Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-08149-860/+1171
| | * | Fix evaluation order in emulation of bitfield assignmentXavier Leroy2021-05-021-2/+2
| | * | Support __builtin_expectXavier Leroy2021-05-021-0/+5
| | * | Support __builtin_unreachableXavier Leroy2021-05-028-2/+32
| | * | Fix spurious error on initialization of struct with flexible array memberXavier Leroy2021-05-021-0/+3
| | * | Update ChangelogXavier Leroy2021-04-291-0/+53
| | * | Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
| | * | MacOS: add a #define __DARWIN_OS_INLINEXavier Leroy2021-04-271-2/+2
| | * | Support Coq 8.13.2Xavier Leroy2021-04-271-2/+2
| | * | More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40