aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLtyping.v
Commit message (Expand)AuthorAgeFilesLines
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-42/+41
* Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-1/+1
* Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-3/+3
* Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-6/+20
|\
| * Value analysis for non trapping loadsDavid Monniaux2019-09-031-0/+14
| * avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-6/+6
* | Refine the type of function results in AST.signatureXavier Leroy2020-02-211-16/+19
|/
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-3/+3
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+2
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-9/+9
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-4/+2
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-80/+80
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-6/+17
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-2/+2
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-74/+105
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+134
* Merge of "newspilling" branch:xleroy2014-07-231-58/+30
* Merge of branch linear-typing:xleroy2014-04-061-252/+176
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-176/+252
* Move wt_instr_inv where it belongs.xleroy2014-03-271-0/+10
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-271-252/+166
* Typo in commentxleroy2013-06-171-1/+1
* Merge of the float32 branch: xleroy2013-05-191-510/+324
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-14/+31
* RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...xleroy2013-03-221-201/+713
* Remove some useless "Require".xleroy2012-12-301-2/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-1/+1
* Merge of the nonstrict-ops branch:xleroy2012-01-141-1/+0
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-2/+3
* Renamed Machconcr into Machsem.xleroy2011-04-091-2/+1
* Merge of branch "unsigned-offsets":xleroy2011-04-091-3/+3
* Support for inlined built-ins.xleroy2010-06-291-4/+26
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-22/+14
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-101-2/+4
* Added support for jump tables in back end.xleroy2009-11-101-0/+14
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-1/+1
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-7/+6
* Added tail call optimization passxleroy2009-03-261-6/+0
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-18/+1
* Revu gestion retaddr et link dans Stackingxleroy2008-04-121-3/+2
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-133/+223
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-221-19/+0
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-2/+2
* Fusion de la branche "traces":xleroy2006-09-041-1003/+227
* Initial import of compcertxleroy2006-02-091-0/+1277
generated by cgit (git 2.34.1) at 2024-05-09 09:06:01 +0000