Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Make reveal axioms from opaque functions quantify over layers | Dan Rosén | 2014-07-10 |
* | New logical encoding of types with Is and IsAlloc | Dan Rosén | 2014-07-07 |
* | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
* | Added support for opaque function definitions, indicated via the {:opaque} at... | Bryan Parno | 2013-12-13 |
* | Fixed let-such-that and if-then-else encodings so that they will pass the sub... | Rustan Leino | 2013-02-21 |
* | Dafny: fixed bug in checking postconditions of functions that mention the res... | Unknown | 2012-08-29 |
* | Dafny: permanently changed the syntax of "datatype" declarations to what prev... | Rustan Leino | 2011-05-27 |
* | Dafny: allow self-calls in function postconditions--these simply refer to the... | rustanleino | 2011-02-03 |