aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-10/+10
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-10/+10
* | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-2/+4
|\|
| * ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-061-2/+4
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-1/+1
|\|
| * Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
* | fixes for ARMDavid Monniaux2019-09-071-0/+7
|/
* Implement a `Osel` operation for ARMXavier Leroy2019-05-201-0/+1
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+2
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ...Michael Schmidt2017-12-151-0/+2
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-3/+3
* ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-171-20/+37
* ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-171-8/+12
* Improve stack offset addressingMichael Schmidt2017-08-021-2/+2
* ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2017-02-131-8/+8
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-27/+32
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-4/+4
* 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-59/+33
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-141/+141
* Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-30/+14
* Updating the PowerPC and ARM ports.Xavier Leroy2015-03-271-3/+6
* Update the ARM port.Xavier Leroy2014-11-241-4/+12
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-16/+19
* Merge of "newspilling" branch:xleroy2014-07-231-5/+4
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-4/+4
* Merge of the "princeton" branch:xleroy2013-06-161-1/+1
* Merge of the float32 branch: xleroy2013-05-191-5/+6
* Update ARM port.xleroy2013-05-171-2/+2
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-40/+39
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-2/+2
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+1
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-257/+207
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-1019/+629
* Pointers one pastxleroy2013-02-151-2/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-2/+4
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-0/+2
* Merge of the nonstrict-ops branch:xleroy2012-01-141-5/+6
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-52/+51
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-4/+3
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-1/+32
* Renamed Machconcr into Machsem.xleroy2011-04-091-53/+53
* Merge of branch "unsigned-offsets":xleroy2011-04-091-63/+98
* Merge of the reuse-temps branch:xleroy2010-09-021-160/+242
* Support for inlined built-ins.xleroy2010-06-291-1/+34
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-2/+11
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-3/+14
* Updating ARM portxleroy2010-03-281-53/+27
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
generated by cgit (git 2.34.1) at 2024-05-08 08:58:01 +0000