aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tunneling.v
Commit message (Expand)AuthorAgeFilesLines
* minor fix in coq2html commentSylvain Boulmé2020-11-161-1/+2
* Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-161-37/+98
* automated writing Compiler.vDavid Monniaux2020-04-221-1/+1
* Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-2/+2
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-061-2/+5
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-3/+1
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-1/+1
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-27/+13
* Remove some useless "Require".xleroy2012-12-301-4/+0
* Updated documentationxleroy2012-08-021-28/+19
* Support for inlined built-ins.xleroy2010-06-291-0/+2
* Added support for jump tables in back end.xleroy2009-11-101-0/+2
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-13/+1
* Added 'going wrong' behaviorsxleroy2009-08-051-29/+22
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-2/+0
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-28/+28
* Fusion de la branche "traces":xleroy2006-09-041-1/+6
* Initial import of compcertxleroy2006-02-091-0/+131