| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 1 | -1/+1 |
| | | |||||
| * | Cleanup | Léo Gourdin | 2020-12-19 | 1 | -46/+0 |
| | | |||||
| * | Some progress in Asmblockgenproof | Léo Gourdin | 2020-12-17 | 1 | -14/+15 |
| | | |||||
| * | intermediatet commit before builtins | Léo Gourdin | 2020-12-16 | 1 | -6/+9 |
| | | |||||
| * | Generals lemmas for asmblockgenproof | Léo Gourdin | 2020-12-14 | 1 | -12/+28 |
| | | |||||
| * | Removing the PseudoAsm IR | Léo Gourdin | 2020-12-13 | 1 | -10/+29 |
| | | |||||
| * | Some cleanup in todos | Léo Gourdin | 2020-12-07 | 1 | -12/+0 |
| | | |||||
| * | a first working draft on ldp/stp peephole | Léo Gourdin | 2020-12-04 | 1 | -16/+16 |
| | | |||||
| * | Adding semantics for Pldp | Léo Gourdin | 2020-12-02 | 1 | -18/+18 |
| | | | | This commit prepare the backend for a peephole optimization in Asmblock. | ||||
| * | Fixing a generation bug on shrx in Asmblockgen | Léo Gourdin | 2020-11-26 | 1 | -0/+6 |
| | | | | I forgot this one and the gen test script reminds me | ||||
| * | This commit fix the issue #226 | Léo Gourdin | 2020-11-26 | 1 | -50/+57 |
| | | | | | - adding two functions to manage special bblock case - adding movz size specifications | ||||
| * | Preparation for postpass in aarch64 and refactoring | Léo Gourdin | 2020-11-02 | 1 | -20/+20 |
| | | |||||
| * | End of Asmblock translation | Léo Gourdin | 2020-10-29 | 1 | -38/+36 |
| | | |||||
| * | Some tests and load/store instr | Léo Gourdin | 2020-10-29 | 1 | -26/+145 |
| | | |||||
| * | If, op, and some tests with a script | Léo Gourdin | 2020-10-28 | 1 | -6/+701 |
| | | |||||
| * | Epilogue OK and loadimm | Léo Gourdin | 2020-10-27 | 1 | -58/+96 |
| | | |||||
| * | Merge remote-tracking branch 'origin/aarch64_asmblockgen' into aarch64_block | Léo Gourdin | 2020-10-27 | 1 | -47/+52 |
| |\ | |||||
| | * | another start for Asmblockgen | Sylvain Boulmé | 2020-10-27 | 1 | -131/+52 |
| | | | |||||
| * | | A more convenient way to handle basic inst | Léo Gourdin | 2020-10-27 | 1 | -99/+18 |
| |/ | |||||
| * | [Draft] Flattened levels of binst | Léo Gourdin | 2020-10-27 | 1 | -49/+180 |
| | | |||||
| * | [Draft] Problems with coercions | Léo Gourdin | 2020-10-26 | 1 | -1078/+166 |
| | | |||||
| * | aarch64 compiles again (but ccomp generates incorrect assembly) | Sylvain Boulmé | 2020-10-23 | 1 | -6/+74 |
| | | |||||
| * | [WIP: Coq compilation broken] Stub for Asmgen | Sylvain Boulmé | 2020-06-21 | 1 | -0/+1197 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |