aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* relecture sylvainSylvain Boulmé2019-04-058-505/+353
* #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-0511-1611/+1634
* Possible fix pour l'issue #82 (mauvais calcul de taille de bundle pour les st...Cyril SIX2019-04-051-1/+1
* Refactorisation de forward_simu_basicCyril SIX2019-04-041-102/+55
* refactorized forward_simu_controlCyril SIX2019-04-041-107/+67
* Refactorisation de forward_simu_par_controlCyril SIX2019-04-041-141/+63
* Erreur idiote dans les latences ?Cyril SIX2019-04-041-2/+2
* Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-0314-1456/+421
|\
| * robustness of Asmblockdeps.*op_eqSylvain Boulmé2019-04-021-27/+38
| * comment on Asmblockdeps.is_constantSylvain Boulmé2019-04-021-9/+12
| * Impure: improved iandb + struct_eqSylvain Boulmé2019-04-013-34/+28
| * renommage abstractbb: Name -> PRegSylvain Boulmé2019-04-015-32/+32
| * renommages abstract_bbSylvain Boulmé2019-04-015-156/+156
| * petite factorisation de preuveSylvain Boulmé2019-04-011-69/+59
| * minor simplSylvain Boulmé2019-04-011-8/+14
| * simpler parexec_wio_bblock_auxSylvain Boulmé2019-04-012-3/+2
| * cleaning Asmvliw semanticsSylvain Boulmé2019-04-014-42/+73
| * delete useless DepExample* filesSylvain Boulmé2019-04-014-1051/+0
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-addr-regCyril SIX2019-04-030-0/+0
|\ \
| * | Revert "Started to add addressing with register + register, Mach -> Asm not d...Cyril SIX2019-04-015-12/+3
| * | Started to add addressing with register + register, Mach -> Asm not done yetCyril SIX2019-04-015-3/+12
* | | Load/Store reg-reg are now proven everywhereCyril SIX2019-04-032-92/+68
* | | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-036-77/+196
* | | Preuve du transl_load et transl_store registre offsetCyril SIX2019-04-032-30/+89
* | | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-033-494/+51
* | | Small refactoring and renaming of Stores and LoadsCyril SIX2019-04-033-70/+50
* | | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-0210-205/+417
* | | Started to add addressing with register + register, Mach -> Asm not done yetCyril SIX2019-04-015-3/+12
|/ /
* / Using fixedd.rz in longofsingle instead of i64_dtosCyril SIX2019-04-012-8/+13
|/
* fix for jump tablesv3.5_k1c_1.0David Monniaux2019-03-302-18/+19
* FIXME: Jumptables have linking issues.David Monniaux2019-03-294-0/+1245
* Merge branch 'mppa_k1c' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-291-8/+8
|\
| * Merge branch 'mppa-mul' into mppa_k0cDavid Monniaux2019-03-2921-1082/+1916
| |\
| * | rm rules that conflictDavid Monniaux2019-03-291-8/+8
* | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mulDavid Monniaux2019-03-2912-72/+235
|\| |
| * | use C99 modeDavid Monniaux2019-03-291-1/+1
| * | Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptableCyril SIX2019-03-291-2/+5
| |\ \
| | * | Finition de la preuve de AsmblockgenproofCyril SIX2019-03-291-2/+5
| * | | Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-292-1/+24
| * | | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-298-24/+1121
| |\ \ \ | | |/ / | |/| |
| | * | No more AdmittedCyril SIX2019-03-291-55/+102
| * | | Avancement dans la preuve du MBjumptableCyril SIX2019-03-291-1/+21
| * | | for testing with questDavid Monniaux2019-03-221-0/+24
| * | | xMerge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-221-0/+3
| |\ \ \
| * | | | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| * | | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| * | | | improved testingDavid Monniaux2019-03-221-5/+16
| * | | | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| * | | | some more testingDavid Monniaux2019-03-221-1/+1
| * | | | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-22302-6460/+51288
| |\ \ \ \
generated by cgit (git 2.34.1) at 2024-07-14 08:37:17 +0000