aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asm.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-061-2/+2
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-031-0/+2
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-211-2/+0
* Implement a `Osel` operation for ARMXavier Leroy2019-05-201-0/+9
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-121-0/+2
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-1/+10
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ...Michael Schmidt2017-12-151-0/+3
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-141-2/+23
* Moved arm eabi fixup to Asmexpand.Bernhard Schommer2017-11-161-2/+25
* ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-171-15/+0
* ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-171-1/+2
* Improve stack offset addressingMichael Schmidt2017-08-021-3/+20
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-4/+6
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-15/+15
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-17/+34
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-58/+58
* Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-26/+21
* Updated the branch and implemented the suggested changes.Bernhard Schommer2015-07-141-17/+31
* Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-1/+38
* Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-261-38/+1
* Moved the printing of the builtin functions etc. into Asmexpand for ARM in th...Bernhard Schommer2015-06-101-1/+38
* Updating the PowerPC and ARM ports.Xavier Leroy2015-03-271-34/+6
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-81/+88
* Merge of "newspilling" branch:xleroy2014-07-231-7/+72
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-10/+4
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-2/+2
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-8/+20
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-53/+117
* Merge of the "princeton" branch:xleroy2013-06-161-1/+1
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-3/+0
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-43/+43
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-99/+114
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-3/+3
* Support for fcmpzd instruction (float compare with +0.0)xleroy2012-03-291-0/+3
* Merge of the "volatile" branch:xleroy2012-02-041-1/+1
* Merge of the nonstrict-ops branch:xleroy2012-01-141-15/+21
* Check fcmpd semanticsxleroy2011-07-311-10/+19
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-66/+77
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-2/+66
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-9/+30
* Merge of branch "unsigned-offsets":xleroy2011-04-091-13/+13
* Merge of the reuse-temps branch:xleroy2010-09-021-8/+5
* Support for inlined built-ins.xleroy2010-06-291-28/+37
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+1
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-1/+1
* Updating ARM portxleroy2010-03-281-3/+7
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-7/+7
* Added support for jump tables.xleroy2009-11-191-1/+22