aboutsummaryrefslogtreecommitdiffstats
path: root/x86/ConstpropOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Support Cygwin 64 bitsXavier Leroy2020-10-051-1/+1
* Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-171-1/+25
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-161-9/+31
* x86 ConstpropOp.addr_strength_reduction: always check validity of resulting a...Xavier Leroy2018-02-081-5/+10
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-051-0/+8
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-171-1/+3
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-24/+24
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+883