aboutsummaryrefslogtreecommitdiffstats
path: root/x86/Op.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-03-011-0/+36
|\
| * Add op for float max and min for x86.Bernhard Schommer2022-02-071-0/+36
* | cond_depends_onDavid Monniaux2020-12-021-7/+7
* | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
* | pointer_eq copiedDavid Monniaux2020-11-251-0/+14
* | porting to ppc riscV x86David Monniaux2020-04-011-3/+8
* | add: non trapping opsDavid Monniaux2019-09-231-0/+31
* | more for passing notrap through x86David Monniaux2019-09-071-0/+13
* | for nontrapDavid Monniaux2019-09-061-0/+28
|/
* Implement a `Osel` operation for x86Xavier Leroy2019-05-201-9/+36
* In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bitsXavier Leroy2018-02-121-5/+21
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+21
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-171-14/+19
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-9/+9
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-8/+8
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+1452
generated by cgit (git 2.34.1) at 2024-05-19 01:05:22 +0000