aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-2/+2
|\
| * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-16/+16
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-3/+3
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-13/+13
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-3/+21
|\ \
| * | ARM generation of 2-instruction signed division by 2 (as opposed to 3-instruc...David Monniaux2020-01-141-3/+21
| |/
* / fixes for ARMDavid Monniaux2019-09-071-3/+5
|/
* Implement a `Osel` operation for ARMXavier Leroy2019-05-201-1/+24
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+2
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ...Michael Schmidt2017-12-151-0/+14
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-4/+4
* ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-171-0/+31
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-12/+12
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-52/+74
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-6/+4
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-142/+142
* Fixed missing unsigned compare for pointer in the arm backend.Bernhard Schommer2015-04-041-2/+4
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-135/+248
* Merge of "newspilling" branch:xleroy2014-07-231-69/+186
* Instead of having two expansions of shrximm (one in SelectOp, one in Asmgen),...xleroy2014-05-281-28/+45
* Eradication of Mfloat64al32, continued.xleroy2014-01-121-2/+0
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-0/+20
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-3/+4
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-130/+304
* Merge of the float32 branch: xleroy2013-05-191-5/+40
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-15/+29
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+2
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-118/+65
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-849/+391
* Pointers one pastxleroy2013-02-151-8/+8
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-5/+9
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-2/+2
* Support for fcmpzd instruction (float compare with +0.0)xleroy2012-03-291-0/+15
* Merge of the nonstrict-ops branch:xleroy2012-01-141-126/+133
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-3/+3
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-6/+38
* Renamed Machconcr into Machsem.xleroy2011-04-091-5/+5
* Merge of branch "unsigned-offsets":xleroy2011-04-091-171/+302
* Merge of the reuse-temps branch:xleroy2010-09-021-574/+503
* 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-2/+2
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-110/+7
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+1507
generated by cgit (git 2.34.1) at 2024-05-08 22:25:27 +0000