aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Debugvarproof.v
Commit message (Expand)AuthorAgeFilesLines
* more proofDavid Monniaux2019-09-051-0/+16
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-6/+6
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-2/+2
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-48/+33
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-62/+62
* Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-2/+4
* Some "feel good" proofs about avail sets.Xavier Leroy2015-08-231-0/+171
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+402