summaryrefslogtreecommitdiff
path: root/common/Globalenvs.v
Commit message (Expand)AuthorAge
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
* CSE: add recognition of some combined operators, conditions, and addressing m...Gravatar xleroy2012-05-26
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* MAJ docGravatar xleroy2012-03-12
* Minor updatesGravatar xleroy2012-03-11
* Merge of Andrew Tolmach's HASP-related changesGravatar xleroy2012-03-09
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
* Memory.v: added drop_perm operationGravatar xleroy2010-09-21
* Merging the Princeton implementation of the memory model. Separate axioms in...Gravatar xleroy2010-06-28
* More faithful semantics for volatile reads and writes.Gravatar xleroy2010-05-23
* - Extended traces so that pointers within globals are supported as event values.Gravatar xleroy2010-05-10
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Ajout find_symbol_not_nullptr; nettoyagesGravatar xleroy2007-12-06
* Ajout de global_addresses_distinctGravatar xleroy2007-11-03
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Revu traitement des variables globales dans AST.program et dans Globalenvs.Gravatar xleroy2006-09-05
* Revu la repartition des sources Coq en sous-repertoiresGravatar xleroy2006-09-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 22:39:28 +0000