aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* fpdivuDavid Monniaux2021-12-171-1/+26
* fix assembly syntaxDavid Monniaux2021-12-121-0/+8
* generate insfDavid Monniaux2021-09-271-32/+32
* more cases detectedDavid Monniaux2021-09-271-1/+33
* recognize insf (missing one case)David Monniaux2021-09-271-0/+23
* Select condition x < 0 with x unsigned leads to falsev3.9_kvx_fix1David Monniaux2021-09-171-3/+105
* replacing omega with lia in some fileLéo Gourdin2021-03-291-18/+19
* Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+9
|\
| * centralize if_sameDavid Monniaux2020-10-091-6/+0
| * do not synthesize select if both operands are identicalDavid Monniaux2020-10-091-0/+15
* | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-281-1/+0
|/
* k1c -> kvx changesDavid Monniaux2020-05-261-0/+1735