aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tailcallproof.v
Commit message (Expand)AuthorAgeFilesLines
* Disable tail calls in variadic functionsMichael Schmidt2023-01-231-5/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-26/+26
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-6/+4
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-2/+2
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-13/+13
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-56/+48
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-62/+62
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-51/+22
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+13
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-3/+7
* Add flags to control individual optimization passes + flag -O0 for turning th...Xavier Leroy2014-11-161-6/+4
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-0/+1
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...xleroy2013-05-171-4/+6
* Merge of the nonstrict-ops branch:xleroy2012-01-141-10/+3
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-6/+4
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+2
* Support for inlined built-ins.xleroy2010-06-291-2/+13
* 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-203/+77
* Added support for jump tables in back end.xleroy2009-11-101-0/+7
* Added 'going wrong' behaviorsxleroy2009-08-051-1/+1
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-4/+4
* Added tail call optimization passxleroy2009-03-261-0/+737