aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/SelectLongproof.v
Commit message (Expand)AuthorAgeFilesLines
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+14
* Remove usage of do.Bernhard Schommer2016-10-041-43/+44
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-23/+247
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-12/+26
* Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-011-0/+304