aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
| | * | Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-245-152/+259
| | * | Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
| | * | Remove `-version-file` option from option summaryXavier Leroy2021-04-231-1/+0
| | * | Move `$` notation in submodule `ClightNotations` and scope `clight_scope`Xavier Leroy2021-04-231-11/+23
| | * | Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-194-36/+16
| | * | Bump minimal Coq version to 8.9.0Xavier Leroy2021-04-191-2/+2
| | * | Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-194-2/+25
| | * | Refactor cparser/Parse.mlXavier Leroy2021-04-191-31/+29
| | * | Ensure compatibility with future versions of MenhirLibXavier Leroy2021-04-191-6/+7
| | * | Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
| * | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-0177-1940/+4260
| |\ \ \
| | * | | removing some Expansion when loading float/single constantsLéo Gourdin2021-06-011-16/+22
| | * | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...Léo Gourdin2021-05-311-1/+0
| | |\ \ \
| | | * | | just remove a debug printLéo Gourdin2021-05-291-1/+0
| | * | | | bugfix A64 peephole (cf Scade/Fighter example)Léo Gourdin2021-05-311-6/+5
| | |/ / /
| | * | | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-198-48/+1410
| | * | | Merge branch 'riscv-work-fpinit-stillexp' into kvx-workLéo Gourdin2021-05-190-0/+0
| | |\ \ \
| | | * | | xorimmsubmission_OOPSLA2021_RISCVLéo Gourdin2021-04-092-0/+77
| | | * | | removing useless flag checkLéo Gourdin2021-04-091-3/+1
| | * | | | debug prints uniformizedLéo Gourdin2021-05-181-69/+66
generated by cgit (git 2.34.1) at 2024-07-04 01:07:00 +0000