aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Added flag to desactivate condition inversionCyril SIX2020-02-031-1/+2
|
* Adding threshold to duplicate instructionsCyril SIX2020-01-311-6/+12
|
* 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-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
| |
generated by cgit (git 2.34.1) at 2024-07-07 06:17:40 +0000