Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | progress in pre_output_regs_correct | Sylvain Boulmé | 2021-02-12 | 1 | -5/+53 | |
| | | | ||||||
| * | | improve the skeleton... | Sylvain Boulmé | 2021-02-11 | 2 | -26/+107 | |
| | | | ||||||
| * | | refactorize inst_checker for checking pre_output_regs | Sylvain Boulmé | 2021-02-11 | 2 | -31/+98 | |
| | | | ||||||
| * | | specification of pre_output_regs for the simulation checker | Sylvain Boulmé | 2021-02-11 | 6 | -125/+107 | |
| | | | ||||||
| * | | factorize lazy_and_Some_* lemmas | Sylvain Boulmé | 2021-02-10 | 1 | -16/+3 | |
| | | | ||||||
* | | | Adding a compiler option -fexpanse-rtlcond | Léo Gourdin | 2021-02-16 | 1 | -1/+3 | |
| | | | ||||||
* | | | [Admitted checker] Some more proof draft | Léo Gourdin | 2021-02-11 | 1 | -97/+272 | |
| | | | ||||||
* | | | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof | Léo Gourdin | 2021-02-11 | 1 | -55/+320 | |
| | | | ||||||
* | | | [Admitted checker] Adding cbranch expansions (without scratch) to the checker | Léo Gourdin | 2021-02-10 | 1 | -3/+93 | |
| | | | ||||||
* | | | [Admitted checker] Checker expansion for reg Ocmp (without scratch) | Léo Gourdin | 2021-02-10 | 3 | -26/+267 | |
| | | | ||||||
* | | | Adding pathmap psize modification during expansion oracle | Léo Gourdin | 2021-02-08 | 1 | -5/+5 | |
| | | | ||||||
* | | | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work | Léo Gourdin | 2021-02-08 | 3 | -12/+212 | |
|\| | | ||||||
| * | | Checker for wellformed path | Léo Gourdin | 2021-02-08 | 1 | -2/+175 | |
| | | | ||||||
| * | | intro RTLpathWFcheck | Sylvain Boulmé | 2021-02-08 | 2 | -4/+32 | |
| |/ | ||||||
| * | Some comment clean on RTLpath | Cyril SIX | 2021-01-19 | 1 | -3/+2 | |
| | | ||||||
* | | cond and branches expanded | Léo Gourdin | 2021-02-06 | 2 | -3/+4 | |
| | | ||||||
* | | Expansion of Ccompimm in RTL [Admitted checker] | Léo Gourdin | 2021-02-02 | 3 | -30/+43 | |
|/ | ||||||
* | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2021-01-07 | 2 | -169/+102 | |
|\ | ||||||
| * | Uniformizing a couple of debug print functions | Cyril SIX | 2020-12-17 | 2 | -87/+28 | |
| | | ||||||
| * | Fixing too many loads being NOTRAP | Cyril SIX | 2020-12-17 | 1 | -3/+9 | |
| | | ||||||
| * | Flushing at each dprintf | Cyril SIX | 2020-12-16 | 1 | -1/+3 | |
| | | ||||||
| * | Partially fixing turning loads into non trap | Cyril SIX | 2020-12-16 | 1 | -22/+56 | |
| | | | | | | | | There are now too many loads turned into non trap. To be investigated | |||||
| * | Cleanup | Cyril SIX | 2020-12-16 | 1 | -83/+0 | |
| | | ||||||
| * | Turning loads into non-trapping when necessary | Cyril SIX | 2020-12-15 | 1 | -1/+34 | |
| | | ||||||
* | | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 1 | -21/+6 | |
| | | ||||||
* | | directory postpass_lib | Sylvain Boulmé | 2021-01-07 | 5 | -0/+0 | |
| | | ||||||
* | | recreate abstractbb/ | Sylvain Boulmé | 2021-01-07 | 4 | -0/+0 | |
| | | ||||||
* | | cleaning | Sylvain Boulmé | 2021-01-07 | 2 | -1440/+0 | |
| | | ||||||
* | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 4 | -25/+28 | |
|\| | ||||||
* | | Merge branch 'kvx-test-prepass' of ↵ | David Monniaux | 2020-11-27 | 11 | -0/+6216 | |
|/ | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass | |||||
* | prepass scheduling proof finished ! | Sylvain Boulmé | 2020-11-20 | 1 | -24/+56 | |
| | | | | proof of the two remaining lemmas | |||||
* | seval_builtin_sval_preserved | David Monniaux | 2020-11-17 | 1 | -1/+4 | |
| | ||||||
* | a little lemma on list of builtins | David Monniaux | 2020-11-17 | 1 | -2/+15 | |
| | ||||||
* | there remains two tricky cases | David Monniaux | 2020-11-16 | 1 | -3/+14 | |
| | ||||||
* | disable debug printing in scheduler | David Monniaux | 2020-11-04 | 1 | -4/+4 | |
| | ||||||
* | simplify HSop (and merge hSop and hSop_Sinit) | Sylvain Boulmé | 2020-10-17 | 2 | -42/+23 | |
| | ||||||
* | fixing the move of the verified prepass scheduler into scheduling/ directory | Sylvain Boulmé | 2020-10-17 | 2 | -758/+872 | |
| | ||||||
* | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verif | Cyril SIX | 2020-10-16 | 6 | -1458/+1452 | |
| | ||||||
* | pour ARM | David Monniaux | 2020-10-02 | 1 | -4/+4 | |
| | ||||||
* | so that all architectures compile | David Monniaux | 2020-10-02 | 1 | -473/+0 | |
| | ||||||
* | attempt at separating the divisions | David Monniaux | 2020-09-29 | 1 | -1/+13 | |
| | ||||||
* | attempt at "zigzag" scheduler; not quite testable due to issues in the ↵ | David Monniaux | 2020-09-24 | 2 | -1/+36 | |
| | | | | duplicate/linearize passes | |||||
* | fix issue 210 in simu_check | Sylvain Boulmé | 2020-09-21 | 1 | -11/+23 | |
| | ||||||
* | more debug info for simu_check | Sylvain Boulmé | 2020-09-21 | 1 | -6/+16 | |
| | ||||||
* | just missing OpWeights for AARCH64 | David Monniaux | 2020-09-16 | 14 | -0/+9446 | |