summaryrefslogtreecommitdiff
path: root/Source/AIFramework
Commit message (Collapse)AuthorAge
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Boogie:Gravatar rustanleino2010-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. ↵Gravatar rustanleino2010-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 assembliesGravatar stobies2009-08-17
|
* Initial set of files.Gravatar mikebarnett2009-07-15