Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | updated the example to include atomic specifications (sent by Suha) | qadeer | 2015-03-29 |
| | |||
* | fixed crash reported by Dan. | qadeer | 2015-03-02 |
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | ||
* | fix from Serdar and Suha | qadeer | 2015-02-24 |
| | |||
* | moved some things around | qadeer | 2015-02-11 |
| | |||
* | minor fix to the golden file | qadeer | 2015-01-28 |
| | |||
* | added lit stuff at the top of the file and the golden output | qadeer | 2015-01-28 |
| | |||
* | Work stealing queue (PLDI '12 Vechev et al.) | Unknown | 2015-01-28 |
| | |||
* | removed unused functions and axioms to make the verification faster | qadeer | 2015-01-27 |
| | |||
* | strengthened type checking | qadeer | 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 ↵ | qadeer | 2014-12-18 |
| | | | | yielding procedures | ||
* | 1. made variable introduction layer explicit in the test cases | qadeer | 2014-12-15 |
| | | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer | ||
* | patched an expected output | qadeer | 2014-12-15 |
| | |||
* | renamed :phase to :layer | qadeer | 2014-11-14 |
| | |||
* | removed a useless procedure | qadeer | 2014-10-21 |
| | |||
* | deleted the free assume about gates after parallel calls | qadeer | 2014-07-26 |
| | |||
* | enabled merging of yield calls | qadeer | 2014-07-20 |
| | |||
* | minor change | qadeer | 2014-07-19 |
| | |||
* | treiber stack fixed | qadeer | 2014-07-18 |
| | |||
* | some clean up | qadeer | 2014-07-16 |
| | |||
* | updated the linear type system based on Chris' design with linear, ↵ | qadeer | 2014-07-15 |
| | | | | linear_in, linear_out | ||
* | simplified yield type chcking and added treiber stack (not fully done) | qadeer | 2014-07-15 |
| | |||
* | added tests | qadeer | 2014-07-12 |
| | |||
* | fixed some tests in og | qadeer | 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 | qadeer | 2014-06-02 |
| | |||
* | Removed old test infrastructure files except for | Dan Liew | 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 | Dan Liew | 2014-05-27 |
| | | | | spaces. | ||
* | Set the following tests to expected failure under lit. Having these | Dan Liew | 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 | Dan Liew | 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 | qadeer | 2014-05-04 |
| | |||
* | second checkpoint | qadeer | 2014-05-04 |
| | |||
* | checkpoint | qadeer | 2014-05-03 |
| | |||
* | updated the mover checks | qadeer | 2014-04-25 |
| | |||
* | added another sample | qadeer | 2014-04-20 |
| | |||
* | added simulation relation computation to yield type checking | qadeer | 2014-04-20 |
| | | | | updated the type check to incorporate {:terminates} annotation | ||
* | added the framing for the refinement check | qadeer | 2014-04-16 |
| | |||
* | added variable hiding | qadeer | 2014-04-16 |
| | | | | added annotation on an atomic action about the phases in which it exists | ||
* | added ReadOnlyStandardVisitor | qadeer | 2014-02-24 |
| | | | | made the default phase of assertions be 0 | ||
* | fixed a bug in desugaring of linear variables | qadeer | 2014-02-20 |
| | |||
* | forgot to update the Answer file earlier | qadeer | 2014-02-12 |
| | |||
* | fixed the civl-paper example | qadeer | 2014-02-12 |
| | |||
* | using break statement in the inner loop instead of goto | qadeer | 2014-02-11 |
| | |||
* | added another example and fixed a bug regarding initialization of pc/ok | qadeer | 2014-02-07 |
| | | | | snapshots per loop header | ||
* | new design for linear types + VCgen | qadeer | 2014-02-07 |
| | | | | | ported all the examples added the QED examples to runtest.bat | ||
* | more cleanup | qadeer | 2014-01-23 |
| | |||
* | some cleanup | qadeer | 2014-01-23 |
| | |||
* | some small optimizations to mover checking | qadeer | 2014-01-22 |
| | | | | added LookUp to multiset.bpl | ||
* | some fixes | qadeer | 2014-01-21 |
| | |||
* | various bug fixes | qadeer | 2014-01-21 |
| | | | | added "cnst" feature | ||
* | fixed a bug revealed subsequent to the latest fix in parallel call handling | qadeer | 2014-01-20 |
| | |||
* | bug fix in handling of parallel call | qadeer | 2014-01-20 |
| |