Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | updated the example to include atomic specifications (sent by Suha) | 2015-03-29 | |
| | |||
* | fixed crash reported by Dan. | 2015-03-02 | |
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | ||
* | fix from Serdar and Suha | 2015-02-24 | |
| | |||
* | moved some things around | 2015-02-11 | |
| | |||
* | minor fix to the golden file | 2015-01-28 | |
| | |||
* | added lit stuff at the top of the file and the golden output | 2015-01-28 | |
| | |||
* | Work stealing queue (PLDI '12 Vechev et al.) | 2015-01-28 | |
| | |||
* | removed unused functions and axioms to make the verification faster | 2015-01-27 | |
| | |||
* | strengthened type checking | 2014-12-26 | |
| | | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions | ||
* | changed type checking of yield procedures so that they can only call other ↵ | 2014-12-18 | |
| | | | | yielding procedures | ||
* | 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 | |
| |