aboutsummaryrefslogtreecommitdiffstats
path: root/common/Memtype.v
Commit message (Expand)AuthorAgeFilesLines
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-10/+10
* Add Mem.free_parallel_inject and use it to simplify Events a bit.xleroy2014-07-311-0/+9
* Merge of "newspilling" branch:xleroy2014-07-231-9/+11
* Merge of the "princeton" branch:xleroy2013-06-161-13/+9
* Pointers one pastxleroy2013-02-151-6/+47
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-0/+1
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-1/+0
* Merge of the newmem branch:xleroy2012-05-211-134/+112
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-091-0/+10
* Merge of the nonstrict-ops branch:xleroy2012-01-141-0/+3
* Back from Oregon commit. xleroy2011-07-051-0/+169
* Merge of branch "unsigned-offsets":xleroy2011-04-091-14/+14
* Memory.v: added drop_perm operationxleroy2010-09-211-0/+50
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-31/+18
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+989