aboutsummaryrefslogtreecommitdiffstats
path: root/backend/SplitLongproof.v
Commit message (Expand)AuthorAgeFilesLines
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-6/+6
* SplitLong: propagate constants through "longofint"Xavier Leroy2016-10-251-2/+3
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-1/+1
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-2/+20
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+1
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-86/+47
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-0/+1142