aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Unusedglobproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'RTL_has_loaded' into kvx-workLéo Gourdin2021-11-021-43/+45
|\
| * Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-43/+45
* | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-1/+1
|\ \ | |/ |/|
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-11/+11
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-11/+11
* | begin scripting the Compiler.v fileDavid Monniaux2020-04-211-2/+2
* | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-1/+31
|/
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-2/+2
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-2/+2
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-7/+7
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+4
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-48/+48
* The subst tactic has become more powerful.Maxime Dénès2017-01-091-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-21/+21
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-221-0/+11
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-509/+611
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-207/+207
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-47/+35
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-17/+17
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+77
* Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-3/+3
* Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-241-0/+1256
generated by cgit (git 2.34.1) at 2024-05-09 17:05:05 +0000