aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-3/+3
|\
| * PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-281-3/+3
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-1/+1
|\|
| * Share code for memory access for PowerPCBernhard Schommer2021-09-061-1/+1
| * Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-241-6/+17
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-6/+17
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-9/+9
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-9/+9
* | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-3/+5
|\|
| * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-061-3/+5
* | PowerPC compilesDavid Monniaux2019-09-071-0/+8
|/
* Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-281-1/+10
* Implement a `Osel` operation for PowerPCXavier Leroy2019-05-201-0/+10
* PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-201-2/+16
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+2
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-10/+33
* Modest optimization of leaf functions (continued)Xavier Leroy2017-04-281-143/+45
* Modest optimization of leaf functionsXavier Leroy2017-04-281-29/+88
* ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2017-02-131-6/+13
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-40/+43
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-3/+3
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-58/+33
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-137/+137
* Adapt the PowerPC port to the new builtin representation.Xavier Leroy2015-08-211-30/+14
* Updating the PowerPC and ARM ports.Xavier Leroy2015-03-271-3/+6
* Update PowerPC port.Xavier Leroy2014-11-241-4/+12
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-181-6/+4
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-9/+15
* Merge of "newspilling" branch:xleroy2014-07-231-5/+9
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-4/+4
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...xleroy2013-12-261-18/+18
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-0/+4
* Merge of the "princeton" branch:xleroy2013-06-161-1/+1
* Merge of the float32 branch: xleroy2013-05-191-3/+2
* Update PowerPC portxleroy2013-05-171-1/+1
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-30/+34
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-4/+6
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-1/+0
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-300/+219
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-1093/+630
* Updated PowerPC port to new integers.xleroy2013-02-121-0/+1
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-2/+7
* Merge of the nonstrict-ops branch:xleroy2012-01-141-3/+21
* Cleaned up old commented-out partsxleroy2011-08-191-8/+0
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-4/+3
* Back from Oregon commit. xleroy2011-07-051-43/+29
* Recognition of rlwimi instruction (useful for bitfield assignment)xleroy2011-06-211-0/+1
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-0/+31
* Renamed Machconcr into Machsem.xleroy2011-04-091-54/+54
generated by cgit (git 2.34.1) at 2024-05-09 10:34:39 +0000