aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* begin implementing -fcse3-conditionsDavid Monniaux2020-12-096-8/+24
* redundant testsDavid Monniaux2020-12-091-0/+11
* CSE3 + conditions proofDavid Monniaux2020-12-092-34/+58
* apply_cond_soundDavid Monniaux2020-12-091-0/+14
* apply_cond0_soundDavid Monniaux2020-12-091-1/+25
* apply_cond1_soundDavid Monniaux2020-12-091-0/+30
* proof for jumptableDavid Monniaux2020-12-091-1/+27
* one 'admit' lessDavid Monniaux2020-12-091-2/+36
* avancement dans les preuvesDavid Monniaux2020-12-091-1/+34
* CSE3 compiles again, but some admitted lemmasDavid Monniaux2020-12-092-11/+9
* progress moving to list of itemsDavid Monniaux2020-12-093-92/+233
* CSE3 with Abst_sameDavid Monniaux2020-12-081-1/+1
* analysis with Abst_sameDavid Monniaux2020-12-083-22/+39
* CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-083-115/+4
* Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-084-555/+242
|\
| * fix new register erasing scheme for AArch64David Monniaux2020-12-083-553/+241
| * rm instructions now unusedDavid Monniaux2020-12-081-2/+1
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-08157-2244/+4035
|\|
| * Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-0818-115/+48
| |\
| | * Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | * ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | * AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| * | Fixing test/regression for KVXv3.8_kvxCyril SIX2020-12-076-2/+409
| * | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-04104-1053/+11993
| |\ \
| | * | CommentCyril SIX2020-12-041-0/+1
| | * | Less aggressive tail duplicationCyril SIX2020-12-041-6/+11
| | * | Clean-up debugCyril SIX2020-12-041-4/+2
| | * | Fixed infinite loop on find_last_node_before_loopCyril SIX2020-12-041-3/+6
| | * | Slight perf improvementCyril SIX2020-12-022-4/+4
| | * | [expensive] Behavior change when the loop has two final instructionsCyril SIX2020-12-021-9/+57
| | * | Duplicateaux: Generalization of look_aheadCyril SIX2020-12-011-3/+5
| * | | Fixing compilation for KVXCyril SIX2020-12-043-2/+7
| * | | still issues with FR in kvxDavid Monniaux2020-12-033-27/+26
| * | | some fixes for KVXDavid Monniaux2020-12-032-6/+0
| * | | fix Makefile pour kvxDavid Monniaux2020-11-191-1/+1
| * | | un peu de progrès sur le MakefileDavid Monniaux2020-11-191-1/+1
| * | | Asmgenproof1 pas sur kvxDavid Monniaux2020-11-191-1/+5
| * | | essai de limitation des paquets KalrayDavid Monniaux2020-11-191-1/+1
| * | | rm unneeded open statements in MLDavid Monniaux2020-11-191-3/+0
| * | | fix MakefileDavid Monniaux2020-11-191-1/+1
| * | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-18133-2071/+3462
| |\ \ \ | | | |/ | | |/|
| | * | Updates for release 3.8v3.8Xavier Leroy2020-11-163-5/+10
| | * | Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
| | * | Support Coq 8.12.1Xavier Leroy2020-11-142-3/+3
| | * | Update READMEXavier Leroy2020-11-091-4/+4
| | * | Update ChangesXavier Leroy2020-11-081-0/+48
| | * | Added semantics for the PowerPC sel and mulh built-insBernhard Schommer2020-11-071-4/+44
| | * | Added missing printer for PowerPC 64 bit comparison.Bernhard Schommer2020-11-061-0/+8
generated by cgit (git 2.34.1) at 2024-06-20 15:12:33 +0000