aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
| |\ | | | | | | | | | | | | Conflicts: mppa_k1c/Asmblockdeps.v
| | * 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
| | | | | | | | | | | | | | | Resource -> PseudoReg macro -> inst
| | * 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
| | | | | | | | | | | | in order to avoid to keep these files up-to-date here...
| * | 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 ↵Cyril SIX2019-04-015-12/+3
| | | | | | | | | | | | | | | | | | | | | | | | done yet" This reverts commit ead2f32a7648d1eb1b828b120821a0b7801c6200.
| | * | 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 ↵Cyril SIX2019-04-036-77/+196
| | | | | | | | | | | | | | | | preuves de Asmblockdeps
| * | | 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 ↵David Monniaux2019-03-291-8/+8
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| | * 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
| | |\ \ \ | | | |/ / | | |/| | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v
| | | * | 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
| | |\ \ \ \
| | * | | | | Jump tables now work. There is still an "Admitted" subcase in a proof.David Monniaux2019-03-223-5/+15
| | | | | | |
| | * | | | | on avance sur la jumptableDavid Monniaux2019-03-222-3/+3
| | | | | | |
generated by cgit (git 2.34.1) at 2024-07-12 02:05:29 +0000