aboutsummaryrefslogtreecommitdiffstats
path: root/x86/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Implement a `Osel` operation for x86Xavier Leroy2019-05-201-21/+143
* x86: wrong modeling of ZF flag for FP comparisonsXavier Leroy2018-12-201-124/+60
* Switching the cases seems to work on x86_32Bernhard Schommer2018-02-121-2/+2
* In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bitsXavier Leroy2018-02-121-2/+7
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+1477