aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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-222-0/+1134
|\
| * 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
| * 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
* | 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-162-1/+3
* | Stub for opcode heuristicCyril SIX2019-12-162-4/+12
* | 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-094-130/+11
|\ \
| * | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-dupl...David Monniaux2019-12-094-130/+11
| |\|
generated by cgit (git 2.34.1) at 2024-06-12 15:34:38 +0000