aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Stackingproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-1/+1
|\
| * removing unusued proof lineLéo Gourdin2021-04-091-1/+0
| * Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-1/+2
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-13/+13
|\ \ | |/ |/|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-13/+13
* | fixes for compiling on other platformsDavid Monniaux2019-09-071-2/+2
* | fixes for ARMDavid Monniaux2019-09-071-2/+3
* | more proofsDavid Monniaux2019-09-051-0/+39
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-271-6/+7
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-6/+1
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-60/+32
|\|
| * Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-171-69/+19
| * Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+24
* | MPPA - Machregs + Conventions1 + backend proof tweakingCyril SIX2018-04-041-1/+6
|/
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-4/+4
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+4
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-76/+76
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-85/+95
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-1/+1
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-51/+68
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-1776/+1030
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-58/+34
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-322/+322
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-53/+58
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-25/+25
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-41/+74
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-4/+12
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-1/+1
* Merge of "newspilling" branch:xleroy2014-07-231-48/+63
* Merge of branch linear-typing:xleroy2014-04-061-117/+90
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-89/+117
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-271-117/+89
* Merge of the "princeton" branch:xleroy2013-06-161-73/+70
* Merge of the float32 branch: xleroy2013-05-191-30/+51
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-353/+466
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-8/+12
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-11/+0
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-031-241/+204
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-200/+245
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-2/+2
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-4/+5
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-3/+3
* Merge of the newmem branch:xleroy2012-05-211-36/+43
* IA32 port: more faithful treatment of pseudoregister ST0.xleroy2011-08-081-70/+124
* 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/+79
* Renamed Machconcr into Machsem.xleroy2011-04-091-10/+10
* Merge of branch "unsigned-offsets":xleroy2011-04-091-939/+1877
* Merge of the reuse-temps branch:xleroy2010-09-021-46/+97
generated by cgit (git 2.34.1) at 2024-05-09 12:12:16 +0000