aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
| * | | more proofsDavid Monniaux2020-01-091-1/+18
| * | | fix bug and forward in proofsDavid Monniaux2020-01-092-2/+18
| * | | some more proofDavid Monniaux2020-01-091-3/+53
| * | | moving forward with proofsDavid Monniaux2020-01-091-1/+59
| * | | fix bug in xfer functionDavid Monniaux2020-01-091-1/+2
| * | | progressing in proofsDavid Monniaux2020-01-082-12/+101
| * | | moving forward in proofsDavid Monniaux2020-01-081-2/+19
| * | | correct semantics for bottomDavid Monniaux2020-01-082-14/+45
| * | | progressing towards a proofDavid Monniaux2020-01-082-47/+150
| * | | bogus proofDavid Monniaux2020-01-081-0/+141
| * | | add an exampleDavid Monniaux2020-01-081-0/+18
| * | | connect forward-moves to compilerDavid Monniaux2020-01-086-6/+23
| * | | I *think* the transformation is now doneDavid Monniaux2020-01-081-2/+57
| * | | transfer functionDavid Monniaux2020-01-081-1/+44
| * | | more on semilattices (ADD_BOTTOM)David Monniaux2020-01-081-4/+114
| * | | continue implementing semilatticeDavid Monniaux2020-01-081-7/+65
| * | | begin latticeDavid Monniaux2020-01-081-0/+57
| |/ /
| * | swap load and store at disjoint offsetsDavid Monniaux2019-12-161-1/+53
| * | swap stores at disjoint offsetsDavid Monniaux2019-12-161-16/+30
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-12-161-1/+1
| |\|
generated by cgit (git 2.34.1) at 2024-07-12 02:52:35 +0000