aboutsummaryrefslogtreecommitdiffstats
path: root/common/Globalenvs.v
Commit message (Expand)AuthorAgeFilesLines
* An improved PTree data structure (#420)Xavier Leroy2021-11-161-9/+0
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-6/+6
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-36/+36
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-1/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-1/+1
* | Remove coq warnings (#28)Bernhard Schommer2017-09-221-8/+8
|/
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-72/+72
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-33/+91
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-3/+4
* Globalenvs: adapt to new linking framework, and revise.Xavier Leroy2016-03-061-1146/+729
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-282/+282
* Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.Xavier Leroy2015-01-231-70/+122
* Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-0/+107
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-4/+78
* Update "read_as_zeros" property.xleroy2014-07-231-1/+3
* Merge of "newspilling" branch:xleroy2014-07-231-3/+3
* Add "read_as_zero" property for memory areas initialized by Init_space.xleroy2014-06-301-14/+106
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-0/+17
* Merge of the "princeton" branch:xleroy2013-06-161-195/+196
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+6
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-12/+17
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-36/+36
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-974/+810
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-7/+6
* Merge of the newmem branch:xleroy2012-05-211-100/+193
* MAJ docv1.10xleroy2012-03-121-0/+1
* Minor updatesxleroy2012-03-111-2/+2
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-091-85/+609
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-45/+163
* Memory.v: added drop_perm operationxleroy2010-09-211-24/+62
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-0/+1
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-83/+110
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-36/+34
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-791/+942
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-53/+53
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Ajout find_symbol_not_nullptr; nettoyagesxleroy2007-12-061-39/+71
* Ajout de global_addresses_distinctxleroy2007-11-031-16/+75
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-173/+517
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-158/+222
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-0/+643
generated by cgit (git 2.34.1) at 2024-05-09 10:07:56 +0000