aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CleanupLabelsproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+1
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* | some more proofs on notrapDavid Monniaux2019-09-051-0/+12
|/
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-2/+2
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-51/+32
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-31/+31
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-7/+3
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-1/+3
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-4/+11
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-15/+37
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-2/+17
* Remove some useless "Require".xleroy2012-12-301-2/+0
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-4/+3
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-4/+6
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-081-0/+336