aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
| |\|
| | * The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
| * | comment out theorem that cannot be provedDavid Monniaux2019-12-141-29/+33
| * | store_store_otherDavid Monniaux2019-12-131-1/+84
| * | progress in chunksDavid Monniaux2019-12-131-45/+9
| * | swap writes in memoryDavid Monniaux2019-12-131-0/+43
| * | set_disjointDavid Monniaux2019-12-131-0/+49
| * | some subgoal was provedDavid Monniaux2019-12-121-6/+61
| * | begin overlap proofsDavid Monniaux2019-12-111-0/+43
* | | 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
* | | 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
| |\| |
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-12-097-124/+74
| | |\|
| | | * Allow Coq 8.10.2.Bernhard Schommer2019-12-031-1/+1
| | | * Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-284-2/+13
generated by cgit (git 2.34.1) at 2024-07-05 10:39:46 +0000