aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Conventions1.v
Commit message (Expand)AuthorAgeFilesLines
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-1/+2
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-22/+22
* In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
* Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-021-3/+14
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-126/+0
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+6
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-15/+13
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-13/+13
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-30/+72
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-2/+24
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-71/+85
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-187/+31
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-38/+38
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-0/+545