Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Removed old test infrastructure files except for | 2014-05-28 | |
| | | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. | ||
* | 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 | ||
* | second checkpoint | 2014-05-04 | |
| | |||
* | updated the mover checks | 2014-04-25 | |
| | |||
* | 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 | ||
* | forgot to update the Answer file earlier | 2014-02-12 | |
| | |||
* | 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 | ||
* | added more information to assert messages | 2014-01-14 | |
| | |||
* | more bug fixes | 2013-12-22 | |
| | |||
* | bug fixes in Duplicate.cs and parsing of invariant attributes | 2013-12-22 | |
| | | | | other bug fixes in QED stuff | ||
* | various updates and tighter integration of QED stuff into mainline | 2013-12-19 | |
| | |||
* | fixed a bug regarding invocation of modsetanalysis w.r.t. OG desugaring | 2013-12-07 | |
| | |||
* | cleaned up the OG code | 2013-08-07 | |
| | | | | enabled it to be always on | ||
* | added another regression | 2013-07-15 | |
| | |||
* | reworked the linear and og implementation based on available variables theory | 2013-05-18 | |
| | |||
* | fixed bug reported by Akash | 2013-05-04 | |
| | |||
* | added free ensures to each procedure to compensate for havocing of allocator | 2013-04-19 | |
| | |||
* | refactored og and fixed latest bug reported by chris | 2013-03-20 | |
| | |||
* | fixed a bug in og | 2013-03-04 | |
| | |||
* | fixed bugs in both parallel calls and linear stuff (reported by Chris) | 2013-03-03 | |
| | | | | also added improved error reporting suggested by Chris | ||
* | bug in OG for parallel call | 2013-03-02 | |
| | |||
* | added parallel calls | 2013-03-01 | |
| | |||
* | fixed another bug reported by ChrisHaw | 2013-02-12 | |
Added an answer file |