aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tailcallproof.v
Commit message (Expand)AuthorAgeFilesLines
* being more archi-independantLéo Gourdin2021-11-021-4/+4
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-45/+28
* Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-2/+2
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-26/+26
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-26/+26
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-0/+37
|\ \ | |/ |/|
| * progress on non trapping loadsDavid Monniaux2019-09-021-8/+32
| * avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-0/+13
* | 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
generated by cgit (git 2.34.1) at 2024-05-09 13:26:23 +0000