aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathSE_impl.v
Commit message (Expand)AuthorAgeFilesLines
* Branch expansions activated and configured in the checker (but admitted) and ...Léo Gourdin2021-02-191-49/+146
* Proof of Ocmp expansions without immediate and some drafts in commentLéo Gourdin2021-02-181-46/+471
* Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-workLéo Gourdin2021-02-161-30/+16
|\
| * specification of pre_output_regs for the simulation checkerSylvain Boulmé2021-02-111-30/+16
* | [Admitted checker] Some more proof draftLéo Gourdin2021-02-111-97/+272
* | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-55/+320
* | [Admitted checker] Adding cbranch expansions (without scratch) to the checkerLéo Gourdin2021-02-101-3/+93
* | [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-17/+261
|/
* simplify HSop (and merge hSop and hSop_Sinit)Sylvain Boulmé2020-10-171-40/+20
* Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-161-1380/+1278
* just missing OpWeights for AARCH64David Monniaux2020-09-161-0/+1631
generated by cgit (git 2.34.1) at 2024-07-12 04:53:34 +0000