aboutsummaryrefslogtreecommitdiffstats
path: root/x86/SelectOp.vp
Commit message (Expand)AuthorAgeFilesLines
* adapt the other targets for the new field in CEcondDavid Monniaux2020-04-081-2/+2
* helpers broke compilationDavid Monniaux2019-07-191-6/+1
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-11/+28
|\
| * x86_64: branchless implementation of floatofintu and intuoffloatXavier Leroy2019-07-171-10/+17
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-1/+6
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-1/+29
|\|
| * Implement a `Osel` operation for x86Xavier Leroy2019-05-201-1/+29
* | ça recompile sur x86David Monniaux2019-03-221-0/+8
|/
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-4/+13
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-4/+4
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+3
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+530