aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Complements.v
Commit message (Expand)AuthorAgeFilesLines
* Simplify module Complements and add separate compilation (#121)Xavier Leroy2018-05-291-74/+172
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-5/+7
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-12/+12
* Merge of the "volatile" branch:xleroy2012-02-041-2/+8
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-174/+130
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-34/+45
* Merge of branches/full-expr-4:xleroy2010-08-181-31/+98
* Support for inlined built-ins.xleroy2010-06-291-2/+10
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+0
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-1/+3
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-9/+7
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-537/+39
* Added 'going wrong' behaviorsxleroy2009-08-051-51/+78
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-1/+1
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-20/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+648