aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-075-0/+15
|
* 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
| |
* | accessors for records are now not extracted it seemsDavid Monniaux2020-02-061-3/+3
|/
* 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
| | | | | | | | | | | | This reverts commit 04a46f516487557df00f43453c8decbc8567c458. It was actually not needed
* | 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 ↵David Monniaux2020-01-142-3/+24
| | | | | | | | | | | | 3-instruction)
| | * 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
| | | | | | | | | | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
| | * Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, using an unknown builtin function was treated like any other call to an undeclared function: a warning was emitted, and an error occurred at link-time. With this commit, using an unknown builtin function is an error, like in Clang.
| | * Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-2114-33/+3
| | | | | | | | | | | | | | | | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
| * | 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
| | | |
generated by cgit (git 2.34.1) at 2024-07-05 06:59:41 +0000