aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* 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
|\|
| * Added description for forward movesCyril SIX2020-01-171-0/+1
| * Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-1512-60/+419
| |\
| | * 2-instruction signed division by two on Aarch64David Monniaux2020-01-153-24/+54
| | * ARM generation of 2-instruction signed division by 2 (as opposed to 3-instruc...David Monniaux2020-01-142-3/+24
| | * 64-bit signed division by two codeDavid Monniaux2020-01-143-14/+26
| | * shrxl_shrl_3David Monniaux2020-01-141-0/+52
| | * shrx'1_shr'David Monniaux2020-01-141-1/+127
| | * rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)David Monniaux2020-01-143-14/+25
| | * shrx_shr_3David Monniaux2020-01-141-0/+54
| | * shrx1_shrDavid Monniaux2020-01-141-0/+51
| | * Remove __builtin_nop from list of x86 builtins.Bernhard Schommer2020-01-031-3/+0
| | * Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-0314-3/+33
| | * Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | * Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-2114-33/+3
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-forwardmovesDavid Monniaux2020-01-092-6/+7
| |\ \
| | * | Fixing issue with <math.h> and fabsCyril SIX2020-01-091-1/+2
| | * | Fixing issue with "destruct ... in ..." tactics with Coq 8.8Cyril SIX2020-01-091-5/+5
| * | | FINISHED the forward-moves passDavid Monniaux2020-01-091-2/+6
| * | | nearly doneDavid Monniaux2020-01-091-3/+5
| * | | fix moveDavid Monniaux2020-01-091-1/+3
| * | | fix moveDavid Monniaux2020-01-092-4/+120
| * | | return is okDavid Monniaux2020-01-091-14/+53
| * | | proof of returnDavid Monniaux2020-01-091-1/+59
| * | | we still have issues with call stacksDavid Monniaux2020-01-092-15/+51
| * | | moving forward with proofsDavid Monniaux2020-01-092-5/+20
| * | | proof for jumptableDavid Monniaux2020-01-091-1/+17
generated by cgit (git 2.34.1) at 2024-07-07 06:20:30 +0000