aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | | Implemented call, return, store and loop heuristicsCyril SIX2019-12-111-2/+55
| | * | | Function to look ahead unconditionallyCyril SIX2019-12-111-0/+12
| | * | | Loop headers detection works!Cyril SIX2019-12-111-3/+17
| | * | | Dominators approach not working well ==> opting for visit approachCyril SIX2019-12-101-23/+73
| | * | | Calcul de dominateurs a l'air de marcherCyril SIX2019-12-101-88/+144
| | * | | Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' into...Cyril SIX2019-12-0924-292/+162
| | |\ \ \
| | | * \ \ Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-dupl...David Monniaux2019-12-0924-292/+162
| | | |\ \ \
| | * | | | | Rajout du calcul de dominateurs - pas testéCyril SIX2019-12-091-16/+43
| | |/ / / /
| | * | | | merge w/ non trapping loadsDavid Monniaux2019-12-061-3/+3
| | * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracleDavid Monniaux2019-12-06199-3768/+22046
| | |\ \ \ \
| | * | | | | Adding breadth first searchCyril SIX2019-12-061-3/+6
| | * | | | | [BROKEN] Compiles, not testedCyril SIX2019-12-061-3/+3
| | * | | | | [BROKEN] Started BFS - does not compileCyril SIX2019-12-051-0/+30
| | * | | | | bfs --> dfsCyril SIX2019-12-051-24/+26
| | * | | | | Traces now stop at Icall/Ibuiltin/IjumptableCyril SIX2019-12-041-6/+11
| | * | | | | Fixed trace selection - for now, it only prints them, and the chosen paths ar...Cyril SIX2019-12-021-17/+32
| | * | | | | [BROKEN] Implementing trace selection from Chang & Hwu 1988, to be debuggedCyril SIX2019-10-091-2/+163
| * | | | | | CSE2 with NOTRAPDavid Monniaux2020-02-032-95/+186
| * | | | | | NOTRAP in CSE2: progressDavid Monniaux2020-02-032-33/+260
| * | | | | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2David Monniaux2020-02-031-18/+18
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2David Monniaux2020-02-035-0/+33
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-288-11/+1865
| |\ \ \ \ \ \ \ \ | | |_|_|_|_|_|/ / | |/| | | | | | |
| * | | | | | | | 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
| * | | | | | | | | 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
generated by cgit (git 2.34.1) at 2024-07-02 00:16:18 +0000