Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | more proofs on notrap2 | David Monniaux | 2019-09-08 | 1 | -9/+53 |
* | more proofs on notrap | David Monniaux | 2019-09-08 | 1 | -6/+124 |
* | moving forward on K1C | David Monniaux | 2019-09-07 | 1 | -35/+19 |
* | more on notrap | David Monniaux | 2019-09-05 | 1 | -8/+26 |
* | (#156) - Un peu de cleaning et de doc | Cyril SIX | 2019-07-30 | 1 | -242/+4 |
* | osel imm | David Monniaux | 2019-06-04 | 1 | -0/+48 |
* | added immediate cmove | David Monniaux | 2019-06-04 | 1 | -0/+3 |
* | shortcuts for cmove | David Monniaux | 2019-06-04 | 1 | -16/+36 |
* | Osel -> assembleur | David Monniaux | 2019-06-04 | 1 | -0/+57 |
* | rm old select/selectl/selectf/selectfs | David Monniaux | 2019-06-03 | 1 | -244/+0 |
* | Asmblockgen prologue is now 1 basicblock (instead of 3) | Cyril SIX | 2019-05-10 | 1 | -25/+22 |
* | Exploiting immediate comparisons | Cyril SIX | 2019-05-09 | 1 | -30/+131 |
* | little fix | David Monniaux | 2019-05-04 | 1 | -1/+1 |
* | rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves) | David Monniaux | 2019-05-03 | 1 | -14/+14 |
* | does not yet work, arity mismatch | David Monniaux | 2019-05-01 | 1 | -0/+1 |
* | it compiles | David Monniaux | 2019-05-01 | 1 | -10/+89 |
* | ça avance | David Monniaux | 2019-05-01 | 1 | -5/+78 |
* | pass one proof | David Monniaux | 2019-05-01 | 1 | -7/+2 |
* | translate load.xs | David Monniaux | 2019-05-01 | 1 | -1/+6 |
* | indexed2XS begin | David Monniaux | 2019-05-01 | 1 | -0/+4 |
* | srsd | David Monniaux | 2019-04-29 | 1 | -11/+9 |
* | begin using shrx | David Monniaux | 2019-04-29 | 1 | -24/+9 |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-refactor | Cyril SIX | 2019-04-08 | 1 | -63/+264 |
|\ | |||||
| * | Oselectf, Oselectfs with condition | David Monniaux | 2019-04-05 | 1 | -17/+111 |
| * | selectl with condition | David Monniaux | 2019-04-05 | 1 | -9/+56 |
| * | Select cmplu | David Monniaux | 2019-04-05 | 1 | -0/+18 |
| * | select cmpu | David Monniaux | 2019-04-05 | 1 | -3/+23 |
| * | factor out some proofs | David Monniaux | 2019-04-05 | 1 | -6/+3 |
| * | some more Oselect comparisons | David Monniaux | 2019-04-04 | 1 | -1/+12 |
| * | Oselect | David Monniaux | 2019-04-04 | 1 | -4/+5 |
| * | prepare for conditions in cmove | David Monniaux | 2019-04-04 | 1 | -4/+4 |
| * | ternary ops for float/double | David Monniaux | 2019-04-03 | 1 | -0/+28 |
| * | ternary ops in AES and TEA | David Monniaux | 2019-04-03 | 1 | -2/+2 |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-03 | 1 | -74/+232 |
| |\ | |||||
| * | | selectl generation | David Monniaux | 2019-03-26 | 1 | -3/+13 |
| * | | selectl | David Monniaux | 2019-03-25 | 1 | -0/+14 |
| * | | more on cmove | David Monniaux | 2019-03-25 | 1 | -63/+24 |
* | | | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactor | Cyril SIX | 2019-04-08 | 1 | -6/+6 |
|\ \ \ | |||||
| * | | | relecture sylvain | Sylvain Boulmé | 2019-04-05 | 1 | -6/+6 |
| | |/ | |/| | |||||
* / | | #91 Removed completely the duplicated semantics in Asmblock | Cyril SIX | 2019-04-05 | 1 | -16/+13 |
|/ / | |||||
* | | Preuve des load/store registre registre. Reste des modifs mineures dans les p... | Cyril SIX | 2019-04-03 | 1 | -29/+157 |
* | | Preuve du transl_load et transl_store registre offset | Cyril SIX | 2019-04-03 | 1 | -25/+84 |
* | | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admitted | Cyril SIX | 2019-04-03 | 1 | -34/+6 |
* | | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet | Cyril SIX | 2019-04-02 | 1 | -13/+12 |
|/ | |||||
* | Enlevé la dépendance mémoire de Pcbu | Cyril SIX | 2019-03-13 | 1 | -3/+3 |
* | Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch | Cyril SIX | 2019-03-08 | 1 | -2/+310 |
|\ | |||||
| * | Preuves du branchement avec des float | Cyril SIX | 2019-03-07 | 1 | -25/+242 |
| * | Fix minor proof | Cyril SIX | 2019-03-07 | 1 | -0/+91 |
* | | remove dep of exec_arith_instr on memory. | Sylvain Boulmé | 2019-03-07 | 1 | -31/+23 |
* | | Experiment Patch of Memory Model | Sylvain Boulmé | 2019-03-07 | 1 | -10/+16 |
|/ |