aboutsummaryrefslogtreecommitdiffstats
path: root/common/Events.v
Commit message (Expand)AuthorAgeFilesLines
...
* Merge of the "volatile" branch:xleroy2012-02-041-231/+266
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-151-0/+176
* Cleaned up old commented-out partsxleroy2011-08-191-21/+0
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-101/+262
* Back from Oregon commit. xleroy2011-07-051-5/+111
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-54/+75
* Merge of branch "unsigned-offsets":xleroy2011-04-091-16/+29
* Semantics of annotationsxleroy2010-09-021-5/+69
* Support for inlined built-ins.xleroy2010-06-291-3/+3
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-247/+363
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-214/+327
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-129/+626
* Existence of behaviorsxleroy2010-01-311-13/+50
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-35/+20
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-3/+3
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-3/+7
* Ajout de common/Complements.vxleroy2007-08-261-1/+79
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-8/+109
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-0/+103