aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Op.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-15/+24
|\
| * PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-281-15/+24
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-2/+1
|\ \
| * | rm instructions now unusedDavid Monniaux2020-12-081-2/+1
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-17/+1
|\| |
| * | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-17/+1
| |\|
| | * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-061-17/+1
| * | op_valid_pointer_eq ppcDavid Monniaux2020-10-191-0/+14
* | | 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/+9
* | trapping opsDavid Monniaux2019-09-241-0/+24
* | PowerPC compilesDavid Monniaux2019-09-071-0/+42
|/
* Implement a `Osel` operation for PowerPCXavier Leroy2019-05-201-9/+34
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+23
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-26/+252
* Replace 'decide equality' in powerpc/Op.v. Bug 21332Bernhard Schommer2017-04-031-4/+5
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-74/+89
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-29/+29
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+16
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-35/+35
* Ccompuimm now depends on the memory, this is needed to proof the Lemma op_dep...Bernhard Schommer2015-04-021-2/+3
* Update PowerPC port.Xavier Leroy2014-11-241-17/+39
* Merge of "newspilling" branch:xleroy2014-07-231-90/+47
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-21/+15
* Merge of branch value-analysis.xleroy2013-12-201-4/+6
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-3/+13
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+10
* Merge of the "princeton" branch:xleroy2013-06-161-2/+2
* Merge of the float32 branch: xleroy2013-05-191-17/+4
* Coq-defined equality functions for Allocation. (continued)xleroy2013-05-011-3/+10
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-10/+45
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+4
* Pointers one pastxleroy2013-02-151-50/+34
* Updated PowerPC port to new integers.xleroy2013-02-121-2/+1
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-8/+8
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-2/+5
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-13/+11
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-071-10/+0
* Improved instruction selection for "notint".xleroy2012-02-241-0/+15
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+55
* Merge of the nonstrict-ops branch:xleroy2012-01-141-660/+605
* Recognition of rlwimi instruction (useful for bitfield assignment)xleroy2011-06-211-3/+12
* Merge of branch "unsigned-offsets":xleroy2011-04-091-97/+230
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-1/+4
* Merge of the reuse-temps branch:xleroy2010-09-021-15/+75
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-26/+15
generated by cgit (git 2.34.1) at 2024-05-09 08:58:31 +0000