aboutsummaryrefslogtreecommitdiffstats
path: root/x86/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* x86 branchless implementation of float -> unsigned int32 conversionfloatofintuXavier Leroy2019-06-071-27/+22
* x86: operators Ointoffloat and Ointofsingle are totalXavier Leroy2019-06-071-2/+4
* x86 branchless implementation of unsigned int32 -> float conversionXavier Leroy2019-06-071-3/+15
* Implement a `Osel` operation for x86Xavier Leroy2019-05-201-0/+26
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-4/+22
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-9/+9
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+10
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+959