aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-1/+1
|\
| * PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-281-1/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-1/+5
|\|
| * Share code for memory access for PowerPCBernhard Schommer2021-09-061-1/+5
| * Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-241-102/+169
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-102/+169
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-30/+30
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-7/+7
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-23/+23
* | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-12/+0
|\|
| * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-061-12/+0
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-12-091-2/+3
|\ \ | |/ |/|
| * PowerPC compilesDavid Monniaux2019-09-071-2/+3
* | Model GPR0 in isel (#199)Xavier Leroy2019-09-171-1/+3
|/
* Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-281-3/+38
* Emulate the "isel" instruction on non-EREF PPC processorsXavier Leroy2019-05-201-2/+2
* Implement a `Osel` operation for PowerPCXavier Leroy2019-05-201-0/+35
* PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-201-37/+114
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-4/+5
* Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-201-3/+8
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-6/+6
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-38/+367
* Modest optimization of leaf functions (continued)Xavier Leroy2017-04-281-0/+56
* Modest optimization of leaf functionsXavier Leroy2017-04-281-11/+70
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-43/+82
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-146/+146
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+12
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-181-69/+58
* Merge of "newspilling" branch:xleroy2014-07-231-64/+71
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-30/+17
* Eradication of Mfloat64al32, continued.xleroy2014-01-121-4/+0
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...xleroy2013-12-261-1/+1
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-32/+112
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-24/+21
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+3
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-935/+489
* Updated PowerPC port to new integers.xleroy2013-02-121-5/+10
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-0/+2
* Improved instruction selection for "notint".xleroy2012-02-241-0/+5
* Merge of the nonstrict-ops branch:xleroy2012-01-141-84/+130
* Cleaned up old commented-out partsxleroy2011-08-191-10/+0
* Back from Oregon commit. xleroy2011-07-051-507/+441
* Recognition of rlwimi instruction (useful for bitfield assignment)xleroy2011-06-211-1/+21
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-3/+35
* Oaddrsymbol and small data areaxleroy2011-06-071-0/+8
* Renamed Machconcr into Machsem.xleroy2011-04-091-5/+5
* Merge of branch "unsigned-offsets":xleroy2011-04-091-26/+28
* Merge of the reuse-temps branch:xleroy2010-09-021-571/+503
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-211-35/+19
* Support for inlined built-ins.xleroy2010-06-291-1/+1
generated by cgit (git 2.34.1) at 2024-05-09 18:28:02 +0000