Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| | | * | Impure: improved iandb + struct_eq | Sylvain Boulmé | 2019-04-01 | 3 | -34/+28 | |
| | | * | renommage abstractbb: Name -> PReg | Sylvain Boulmé | 2019-04-01 | 5 | -32/+32 | |
| | | * | renommages abstract_bb | Sylvain Boulmé | 2019-04-01 | 5 | -156/+156 | |
| | | * | petite factorisation de preuve | Sylvain Boulmé | 2019-04-01 | 1 | -69/+59 | |
| | | * | minor simpl | Sylvain Boulmé | 2019-04-01 | 1 | -8/+14 | |
| | | * | simpler parexec_wio_bblock_aux | Sylvain Boulmé | 2019-04-01 | 2 | -3/+2 | |
| | | * | cleaning Asmvliw semantics | Sylvain Boulmé | 2019-04-01 | 4 | -42/+73 | |
| | | * | delete useless DepExample* files | Sylvain Boulmé | 2019-04-01 | 4 | -1051/+0 | |
| | * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-addr-reg | Cyril SIX | 2019-04-03 | 0 | -0/+0 | |
| | |\ \ | ||||||
| | * | | | Load/Store reg-reg are now proven everywhere | Cyril SIX | 2019-04-03 | 2 | -92/+68 | |
| | * | | | Preuve des load/store registre registre. Reste des modifs mineures dans les p... | Cyril SIX | 2019-04-03 | 6 | -77/+196 | |
| | * | | | Preuve du transl_load et transl_store registre offset | Cyril SIX | 2019-04-03 | 2 | -30/+89 | |
| | * | | | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admitted | Cyril SIX | 2019-04-03 | 3 | -494/+51 | |
| | * | | | Small refactoring and renaming of Stores and Loads | Cyril SIX | 2019-04-03 | 3 | -70/+50 | |
| | * | | | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet | Cyril SIX | 2019-04-02 | 10 | -205/+417 | |
| | * | | | Started to add addressing with register + register, Mach -> Asm not done yet | Cyril SIX | 2019-04-01 | 5 | -3/+12 | |
* | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-02 | 32 | -1238/+1672 | |
|\ \ \ \ \ | | |_|/ / | |/| | | | ||||||
| * | | | | Revert "Started to add addressing with register + register, Mach -> Asm not d... | Cyril SIX | 2019-04-01 | 5 | -12/+3 | |
| * | | | | Started to add addressing with register + register, Mach -> Asm not done yet | Cyril SIX | 2019-04-01 | 5 | -3/+12 | |
| | |/ / | |/| | | ||||||
| * | | | Using fixedd.rz in longofsingle instead of i64_dtos | Cyril SIX | 2019-04-01 | 2 | -8/+13 | |
| | |/ | |/| | ||||||
| * | | fix for jump tablesv3.5_k1c_1.0 | David Monniaux | 2019-03-30 | 2 | -18/+19 | |
| * | | FIXME: Jumptables have linking issues. | David Monniaux | 2019-03-29 | 4 | -0/+1245 | |
| * | | Merge branch 'mppa_k1c' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-29 | 1 | -8/+8 | |
| |\ \ | ||||||
| | * \ | Merge branch 'mppa-mul' into mppa_k0c | David Monniaux | 2019-03-29 | 21 | -1082/+1916 | |
| | |\ \ | ||||||
| | * | | | rm rules that conflict | David Monniaux | 2019-03-29 | 1 | -8/+8 | |
| * | | | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mul | David Monniaux | 2019-03-29 | 12 | -72/+235 | |
| |\| | | | ||||||
| | * | | | use C99 mode | David Monniaux | 2019-03-29 | 1 | -1/+1 | |
| | * | | | Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptable | Cyril SIX | 2019-03-29 | 1 | -2/+5 | |
| | |\ \ \ | ||||||
| | | * | | | Finition de la preuve de Asmblockgenproof | Cyril SIX | 2019-03-29 | 1 | -2/+5 | |
| | * | | | | Preuve de Jumptable dans Asmblockdeps.v | Cyril SIX | 2019-03-29 | 2 | -1/+24 | |
| | * | | | | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptable | Cyril SIX | 2019-03-29 | 8 | -24/+1121 | |
| | |\ \ \ \ | | | |/ / / | | |/| | | | ||||||
| | | * | | | No more Admitted | Cyril SIX | 2019-03-29 | 1 | -55/+102 | |
| | * | | | | Avancement dans la preuve du MBjumptable | Cyril SIX | 2019-03-29 | 1 | -1/+21 | |
| | * | | | | for testing with quest | David Monniaux | 2019-03-22 | 1 | -0/+24 | |
| | * | | | | xMerge branch 'mppa-mul' into mppa-jumptable | David Monniaux | 2019-03-22 | 1 | -0/+3 | |
| | |\ \ \ \ | ||||||
| | * | | | | | check that gcc and ccomp compiled k1c code return the same | David Monniaux | 2019-03-22 | 1 | -2/+6 | |
| | * | | | | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd) | David Monniaux | 2019-03-22 | 1 | -1/+1 | |
| | * | | | | | improved testing | David Monniaux | 2019-03-22 | 1 | -5/+16 | |
| | * | | | | | uses yarpgen random generator | David Monniaux | 2019-03-22 | 1 | -0/+37 | |
| | * | | | | | some more testing | David Monniaux | 2019-03-22 | 1 | -1/+1 | |
| | * | | | | | Merge branch 'mppa-mul' into mppa-jumptable | David Monniaux | 2019-03-22 | 302 | -6460/+51288 | |
| | |\ \ \ \ \ | ||||||
| | * | | | | | | Jump tables now work. There is still an "Admitted" subcase in a proof. | David Monniaux | 2019-03-22 | 3 | -5/+15 | |
| | * | | | | | | on avance sur la jumptable | David Monniaux | 2019-03-22 | 2 | -3/+3 | |
| | * | | | | | | jumptable avance | David Monniaux | 2019-03-22 | 1 | -1/+8 | |
| | * | | | | | | Fixed proof of Asmblockdeps wrt Pjumptable | Cyril SIX | 2019-03-22 | 1 | -25/+28 | |
| | * | | | | | | begin jumptables (does not work) | David Monniaux | 2019-03-21 | 5 | -8/+57 | |
| * | | | | | | | missing config.h | David Monniaux | 2019-03-29 | 1 | -0/+3 | |
| * | | | | | | | Makefile for picosat | David Monniaux | 2019-03-29 | 3 | -62/+0 | |
| | |_|_|_|/ / | |/| | | | | | ||||||
| * | | | | | | ocaml benchmark | David Monniaux | 2019-03-28 | 3 | -8/+22 | |
| * | | | | | | Makefile | David Monniaux | 2019-03-28 | 5 | -1025/+35 |