aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* ternary ops for float/doubleDavid Monniaux2019-04-036-14/+116
* for floats and doubles, asmgen supportDavid Monniaux2019-04-033-15/+92
* ternary ops in AES and TEADavid Monniaux2019-04-037-21/+14
* Merge branch 'mppa-ternary' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Com...David Monniaux2019-04-0334-2223/+1151
|\
| * problem in ValueAOpDavid Monniaux2019-04-038-22/+37
| * begin implementing ternary builtinDavid Monniaux2019-04-032-4/+20
| * selection of builtin.. progress...David Monniaux2019-04-031-13/+14
| * some more on builtinsDavid Monniaux2019-04-032-3/+20
| * attempts at generating builtins, startDavid Monniaux2019-04-033-14/+16
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-0350-3401/+2712
| |\
| | * 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
| | |\ \
| | * | | 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
* | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-0232-1238/+1672
|\ \ \ \ \ | | |_|/ / | |/| | |
| * | | | 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
| | |/ / | |/| |
| * | | 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
generated by cgit (git 2.34.1) at 2024-07-04 12:04:33 +0000