aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Archi.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-2/+1
|\
| * Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
* | test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
|/
* Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
* Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-021-0/+3
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-0/+5
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-13/+17
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+14
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-6/+6
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-3/+12
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+2
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-2/+2
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+4
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-1/+4
* Merge of "newspilling" branch:xleroy2014-07-231-3/+11
* PowerPC is big-endian, dammit.xleroy2014-02-211-2/+2
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-0/+34