aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-032176-666/+596149
|\
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-1451-456/+2436
| |\
| | * Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-124-4/+59
| | * Moving some arch specific theorems from PSproof to AsmblockpropsCyril SIX2020-02-112-219/+218
| | * Moving Asmblockgenproof0 to mppa_k1c/lib/Cyril SIX2020-02-101-0/+0
| | * Removing from Asmblockgenproof0 architecture specific definitionsCyril SIX2020-02-109-130/+153
| | * Moved some theoremsCyril SIX2020-02-104-113/+101
| | * bringing back the ppc64 runtimeDavid Monniaux2020-02-095-0/+440
| | * Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2020-02-0817-0/+1430
| | |\
| | | * why did we remove the ppc runtime ?!David Monniaux2020-02-0817-0/+1430
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-0812-54/+84
| | |\ \ | | | |/ | | |/|
| | * | stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-075-0/+15
| * | | Merge branch 'mppa-work' into mppa-cse2Cyril SIX2020-02-064-67/+87
| |\| |
| | * | Merge branch 'mppa-fixing-bundling' into mppa-workCyril SIX2020-02-064-67/+87
| | |\ \
| | | * | Fixing maddw and maddd resource tablesCyril SIX2020-02-061-2/+19
| | | * | Using Ocaml type instead of string to identify resourcesCyril SIX2020-02-061-35/+36
| | | * | Fixed reservation tablesCyril SIX2020-02-061-44/+46
| | | * | Breaking the prologue to satisfy resource constraintsCyril SIX2020-02-061-1/+1
| | | * | Fixed using ccomp assembly preprocessorCyril SIX2020-02-061-3/+3
| | | * | Using k1-elf-as instead of k1-cos-gcc for assemblingCyril SIX2020-02-031-2/+2
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-3/+3
| |\| | |
| | * | | accessors for records are now not extracted it seemsDavid Monniaux2020-02-061-3/+3
| | |/ /
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-0616-66/+832
| |\| |
| | * | Added flag to desactivate condition inversionCyril SIX2020-02-033-1/+6
| | * | Adding threshold to duplicate instructionsCyril SIX2020-01-311-6/+12
| | * | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracleCyril SIX2020-01-277-42/+187
| | |\ \
| | | * | Updated scripts to run the tests on test/mppaCyril SIX2020-01-275-7/+19
| | | * | Hardware runs for test/mppa/interopCyril SIX2020-01-271-24/+113
| | | * | New directive hardtest and hardcheck to run on hardware test/mppa/instrCyril SIX2020-01-271-11/+55
| | * | | Tail duplication optimization defaulting to offCyril SIX2020-01-272-2/+1
| | * | | Added a flag to desactivate tail duplicationCyril SIX2020-01-275-6/+17
| | * | | Added debug message when inverting ifso ifnotCyril SIX2020-01-241-1/+3
| | * | | Oracle inverting branches when trace does not go in fallthruCyril SIX2020-01-241-2/+21
| | * | | Revert "Modified the hook for the oracle"Cyril SIX2020-01-233-12/+8
| | * | | Verificator finished for handling reversed IcondCyril SIX2020-01-232-11/+18
| | * | | Added clause in match_inst to allow Icond reversalCyril SIX2020-01-231-4/+13
| | * | | Modified the hook for the oracleCyril SIX2020-01-233-8/+12
| | * | | Fixing bug caused by get_predecessors returning duplicatesCyril SIX2020-01-231-5/+8
| | * | | Printing traces right before duplicatingCyril SIX2020-01-231-5/+2
| | * | | Fixing bug (used physical instead of structural inequality)Cyril SIX2020-01-221-1/+2
| | * | | Merge branch 'mppa-work' into mppa-duplicate-oracleCyril SIX2020-01-2226-68/+1905
| | |\| |
| | * | | Fixing is_empty functionCyril SIX2020-01-221-3/+3
| | * | | Branch duplication implementationCyril SIX2020-01-221-12/+94
| | * | | Set up the groundbase for doing the duplicationCyril SIX2020-01-171-4/+14
| | * | | Removed unnecessary .mli file (provoked compilation problems)Cyril SIX2020-01-171-12/+0
| | * | | Adding more debug elementsCyril SIX2020-01-151-1/+9
| | * | | Typo in printfCyril SIX2020-01-131-1/+1
| | * | | Opcode heuristic done for K1cCyril SIX2019-12-163-3/+33
| | * | | Stub for opcode heuristicCyril SIX2019-12-163-4/+16
| | * | | Fixing loop heuristic for the way CompCert handles loopsCyril SIX2019-12-111-11/+19
generated by cgit (git 2.34.1) at 2024-06-30 00:00:59 +0000