summaryrefslogtreecommitdiff
path: root/Test/og/DeviceCache.bpl
Commit message (Expand)AuthorAge
* renamed og to civlGravatar qadeer2015-04-22
* strengthened type checkingGravatar qadeer2014-12-26
* changed type checking of yield procedures so that they can only call other yi...Gravatar qadeer2014-12-18
* 1. made variable introduction layer explicit in the test casesGravatar qadeer2014-12-15
* renamed :phase to :layerGravatar qadeer2014-11-14
* updated the linear type system based on Chris' design with linear, linear_in,...Gravatar qadeer2014-07-15
* simplified yield type chcking and added treiber stack (not fully done)Gravatar qadeer2014-07-15
* Fix lit test suite when running Boogie under a path that containsGravatar Dan Liew2014-05-27
* Enable as many "og" lit tests. Several fail because they weren'tGravatar Dan Liew2014-05-11
* second checkpointGravatar qadeer2014-05-04
* checkpointGravatar qadeer2014-05-03
* added simulation relation computation to yield type checkingGravatar qadeer2014-04-20
* new design for linear types + VCgenGravatar qadeer2014-02-07
* fixed a bug revealed subsequent to the latest fix in parallel call handlingGravatar qadeer2014-01-20
* a fix regarding the checking of assertions in atomic specs at call sitesGravatar qadeer2014-01-08
* another fixGravatar qadeer2014-01-02
* some more fixes to examplesGravatar qadeer2014-01-02
* more fixesGravatar qadeer2014-01-02
* some more fixesGravatar qadeer2014-01-02
* fixed examples to deal with yield type checking errorsGravatar qadeer2014-01-01
* more bug fixesGravatar qadeer2013-12-24
* updatesGravatar qadeer2013-12-23
* various updates and tighter integration of QED stuff into mainlineGravatar qadeer2013-12-19
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
* fixed type checking errors in QED stuffGravatar qadeer2013-12-14
* some refactoring of QED stuffGravatar qadeer2013-12-10
* first check inGravatar qadeer2013-12-04