aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tunnelingproof.v
Commit message (Expand)AuthorAgeFilesLines
* Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-171-666/+0
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-7/+6
|\
| * Improve branch tunnelingXavier Leroy2021-01-131-36/+217
| * Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-4/+4
* | Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-161-217/+287
* | automated writing Compiler.vDavid Monniaux2020-04-221-1/+1
* | more proofs going throughDavid Monniaux2019-09-051-0/+25
|/
* Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-171-2/+4
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-1/+9
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Tunnelingproof: Remove assumption destroyed_by_cond c = nil.Xavier Leroy2017-05-021-66/+210
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-061-29/+36
* 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-32/+26
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-33/+33
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-8/+2
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-2/+3
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-4/+9
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-82/+112
* Merge of the nonstrict-ops branch:xleroy2012-01-141-7/+2
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-15/+14
* Support for inlined built-ins.xleroy2010-06-291-0/+8
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+6
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-0/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-6/+5
* Added support for jump tables in back end.xleroy2009-11-101-0/+7
* Added 'going wrong' behaviorsxleroy2009-08-051-108/+113
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-2/+4
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-6/+0
* MAJ documentationxleroy2008-07-271-1/+1
* Simplification de la semantique de LTL et LTLin. Les details lies aux conven...xleroy2008-07-251-20/+9
* Nettoyage du traitement des signatures au return dans LTL et LTLinxleroy2008-07-071-9/+9
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-212/+260
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-3/+3
* Fusion de la branche "traces":xleroy2006-09-041-62/+74
* Initial import of compcertxleroy2006-02-091-0/+311
generated by cgit (git 2.34.1) at 2024-06-02 18:40:50 +0000