aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathScheduler.v
Commit message (Expand)AuthorAgeFilesLines
* rm "Admitted"David Monniaux2021-07-161-11/+10
* Deactivate sched validator (i think)nicolas.nardino2021-07-081-10/+11
* Adding fp init expansionsLéo Gourdin2021-03-021-3/+3
* [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-021-3/+3
* [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-7/+3
* Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-workLéo Gourdin2021-02-081-9/+9
|\
| * intro RTLpathWFcheckSylvain Boulmé2021-02-081-4/+4
* | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-11/+14
|/
* Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-161-5/+2
* just missing OpWeights for AARCH64David Monniaux2020-09-161-0/+333