aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Renumberproof.v
Commit message (Expand)AuthorAgeFilesLines
* being more archi-independantLéo Gourdin2021-11-021-2/+2
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-66/+67
* avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-0/+12
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-30/+26
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-34/+34
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-7/+1
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+7
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-3/+8
* Change interface of Kildall solvers to avoid precomputing the map pc -> list ...xleroy2013-08-121-5/+5
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-2/+2
* Remove some useless "Require".xleroy2012-12-301-3/+0
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-2/+4
* Merge of the newmem branch:xleroy2012-05-211-0/+268