Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | rustanleino | 2010-08-10 |
| | | | | input). | ||
* | Boogie: Removed trailing spaces in code | tabarbe | 2010-08-04 |
| | |||
* | Boogie: | rustanleino | 2010-05-15 |
| | | | | | | | | | | * Added support for polymorphism in lambda expressions * Little clean-up here and there * Added 'then' keyword to emacs and latex modes Dafny: * Added support for fine-grained framing, using the back-tick syntax from Region Logic * Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses | ||
* | * Added "deprecated" comment in help message about /interprocInfer switch. ↵ | rustanleino | 2010-02-18 |
| | | | | | | | The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods | ||
* | Sign assemblies | stobies | 2009-08-17 |
| | |||
* | Initial set of files. | mikebarnett | 2009-07-15 |