summaryrefslogtreecommitdiff
path: root/Test/og/Answer
Commit message (Collapse)AuthorAge
* Removed old test infrastructure files except forGravatar Dan Liew2014-05-28
| | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
* Enable as many "og" lit tests. Several fail because they weren'tGravatar Dan Liew2014-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 checkpointGravatar qadeer2014-05-04
|
* updated the mover checksGravatar qadeer2014-04-25
|
* added the framing for the refinement checkGravatar qadeer2014-04-16
|
* added variable hidingGravatar qadeer2014-04-16
| | | | added annotation on an atomic action about the phases in which it exists
* added ReadOnlyStandardVisitorGravatar qadeer2014-02-24
| | | | made the default phase of assertions be 0
* forgot to update the Answer file earlierGravatar qadeer2014-02-12
|
* added another example and fixed a bug regarding initialization of pc/okGravatar qadeer2014-02-07
| | | | snapshots per loop header
* new design for linear types + VCgenGravatar qadeer2014-02-07
| | | | | ported all the examples added the QED examples to runtest.bat
* added more information to assert messagesGravatar qadeer2014-01-14
|
* more bug fixesGravatar qadeer2013-12-22
|
* bug fixes in Duplicate.cs and parsing of invariant attributesGravatar qadeer2013-12-22
| | | | other bug fixes in QED stuff
* various updates and tighter integration of QED stuff into mainlineGravatar qadeer2013-12-19
|
* fixed a bug regarding invocation of modsetanalysis w.r.t. OG desugaringGravatar qadeer2013-12-07
|
* cleaned up the OG codeGravatar qadeer2013-08-07
| | | | enabled it to be always on
* added another regressionGravatar qadeer2013-07-15
|
* reworked the linear and og implementation based on available variables theoryGravatar Unknown2013-05-18
|
* fixed bug reported by AkashGravatar Unknown2013-05-04
|
* added free ensures to each procedure to compensate for havocing of allocatorGravatar Unknown2013-04-19
|
* refactored og and fixed latest bug reported by chrisGravatar Unknown2013-03-20
|
* fixed a bug in ogGravatar Unknown2013-03-04
|
* fixed bugs in both parallel calls and linear stuff (reported by Chris)Gravatar Unknown2013-03-03
| | | | also added improved error reporting suggested by Chris
* bug in OG for parallel callGravatar Unknown2013-03-02
|
* added parallel callsGravatar Unknown2013-03-01
|
* fixed another bug reported by ChrisHawGravatar Unknown2013-02-12
Added an answer file