aboutsummaryrefslogtreecommitdiffstats
path: root/arm/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-2/+2
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-2/+2
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-201-2/+2
|\|
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-11/+16
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-10/+15
| * ARM: select is not supported at type TlongXavier Leroy2019-06-061-1/+3
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-0/+16
|\ \
| * | ARM: select is not supported at type TlongXavier Leroy2019-06-011-1/+3
| |/
| * Implement a `Osel` operation for ARMXavier Leroy2019-05-201-0/+14
* | ARM repasseDavid Monniaux2019-03-221-2/+26
|/
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+1
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+10
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-8/+9
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-90/+90
* Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-3/+5
* Updating the PowerPC and ARM ports.Xavier Leroy2015-03-271-0/+15
* Merge of "newspilling" branch:xleroy2014-07-231-0/+76
* Instead of having two expansions of shrximm (one in SelectOp, one in Asmgen),...xleroy2014-05-281-38/+2
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-2/+2
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-13/+36
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-12/+2
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-44/+64
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-7/+15
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-15/+15
* Remove some useless "Require".xleroy2012-12-301-2/+0
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-70/+75
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-8/+4
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-241-0/+15
* Merge of the "volatile" branch:xleroy2012-02-041-0/+25
* Merge of the nonstrict-ops branch:xleroy2012-01-141-758/+503
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-40/+9
* Merge of branch "unsigned-offsets":xleroy2011-04-091-41/+44
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-2/+2
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-12/+21
* Merge of the reuse-temps branch:xleroy2010-09-021-54/+89
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-10/+10
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-0/+986
generated by cgit (git 2.34.1) at 2024-05-08 16:58:57 +0000