Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 1. made variable introduction layer explicit in the test cases | 2014-12-15 | |
| | | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer | ||
* | patched an expected output | 2014-12-15 | |
| | |||
* | renamed :phase to :layer | 2014-11-14 | |
| | |||
* | removed a useless procedure | 2014-10-21 | |
| | |||
* | deleted the free assume about gates after parallel calls | 2014-07-26 | |
| | |||
* | enabled merging of yield calls | 2014-07-20 | |
| | |||
* | minor change | 2014-07-19 | |
| | |||
* | treiber stack fixed | 2014-07-18 | |
| | |||
* | some clean up | 2014-07-16 | |
| | |||
* | updated the linear type system based on Chris' design with linear, ↵ | 2014-07-15 | |
| | | | | linear_in, linear_out | ||
* | simplified yield type chcking and added treiber stack (not fully done) | 2014-07-15 | |
| | |||
* | added tests | 2014-07-12 | |
| | |||
* | fixed some tests in og | 2014-07-11 | |
| | | | | | added another test in linear (based on bug reported by Chris) removed the QED build configuration | ||
* | updated golden outputs and removed irrelevant tests | 2014-06-02 | |
| | |||
* | Removed old test infrastructure files except for | 2014-05-28 | |
| | | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. | ||
* | Fix lit test suite when running Boogie under a path that contains | 2014-05-27 | |
| | | | | spaces. | ||
* | Set the following tests to expected failure under lit. Having these | 2014-05-19 | |
| | | | | | | | | | | | | | | | reported is unnecessary noise right now. Someone needs to fix these tests but I'm not the author. Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl Boogie :: test21/Maps2.bpl Boogie :: test21/test3_AddMethod_conv.bpl | ||
* | Enable as many "og" lit tests. Several fail because they weren't | 2014-05-11 | |
| | | | | | | | | | | | | being executed previously! Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl | ||
* | example for variable introduction added | 2014-05-04 | |
| | |||
* | second checkpoint | 2014-05-04 | |
| | |||
* | checkpoint | 2014-05-03 | |
| | |||
* | updated the mover checks | 2014-04-25 | |
| | |||
* | added another sample | 2014-04-20 | |
| | |||
* | added simulation relation computation to yield type checking | 2014-04-20 | |
| | | | | updated the type check to incorporate {:terminates} annotation | ||
* | added the framing for the refinement check | 2014-04-16 | |
| | |||
* | added variable hiding | 2014-04-16 | |
| | | | | added annotation on an atomic action about the phases in which it exists | ||
* | added ReadOnlyStandardVisitor | 2014-02-24 | |
| | | | | made the default phase of assertions be 0 | ||
* | fixed a bug in desugaring of linear variables | 2014-02-20 | |
| | |||
* | forgot to update the Answer file earlier | 2014-02-12 | |
| | |||
* | fixed the civl-paper example | 2014-02-12 | |
| | |||
* | using break statement in the inner loop instead of goto | 2014-02-11 | |
| | |||
* | added another example and fixed a bug regarding initialization of pc/ok | 2014-02-07 | |
| | | | | snapshots per loop header | ||
* | new design for linear types + VCgen | 2014-02-07 | |
| | | | | | ported all the examples added the QED examples to runtest.bat | ||
* | more cleanup | 2014-01-23 | |
| | |||
* | some cleanup | 2014-01-23 | |
| | |||
* | some small optimizations to mover checking | 2014-01-22 | |
| | | | | added LookUp to multiset.bpl | ||
* | some fixes | 2014-01-21 | |
| | |||
* | various bug fixes | 2014-01-21 | |
| | | | | added "cnst" feature | ||
* | fixed a bug revealed subsequent to the latest fix in parallel call handling | 2014-01-20 | |
| | |||
* | bug fix in handling of parallel call | 2014-01-20 | |
| | |||
* | updates | 2014-01-16 | |
| | |||
* | Merge | 2014-01-16 | |
|\ | |||
* | | updating treiber stack | 2014-01-16 | |
| | | |||
| * | yields with invariants factored out into Yield12 | 2014-01-16 | |
|/ | |||
* | InsertPair added. | 2014-01-15 | |
| | |||
* | Added Treiber stack (not yet readable by QED version of Boogie.) | 2014-01-15 | |
| | |||
* | Added Multiset benchmark | 2014-01-15 | |
| | |||
* | added more information to assert messages | 2014-01-14 | |
| | |||
* | small update to the example | 2014-01-09 | |
| | |||
* | a fix regarding the checking of assertions in atomic specs at call sites | 2014-01-08 | |
| |