| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
|
| | |
|
| |
|
|
| |
Make the set class generic
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
|
| |
|
|
| |
configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
|
| | |
|
| |
|
|
| |
Select 4.0 client profile on all projects
|
| |
|
|
| |
structure instead
|
| |
|
|
| |
Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
|
| |
|
|
|
|
| |
* enhanced the printing of captured states
* addressed some warnings issued by VS 2010
* some code formatting
|
| | |
|
| |
|
|
|
| |
only this target has a compile time dependency on Microsoft.Z3.dll.
To compile this target, a reference to z3api must be manually added to BoogieDriver.
|
| |
|
|
| |
fewer error messages when compiling with runtime checking on.
|
| |
|
|
| |
doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
|
| |
|
|
| |
project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
|
| |
|
|
| |
Z3api.csproj shouldn't get in the way this time 'round.
|
| |
|
|
| |
files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
|
| |
|
|
| |
unnecessarry one.
|
| | |
|
| |
|
|
| |
port of the project
|
| |
|
|
| |
input).
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
* 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
|
| |
|
|
|
|
|
| |
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
|
| | |
|
| |
|
Dan Liew
Ally Donaldson
Michal Moskal
Rustan Leino