| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
| |
implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
|
|
| |
files generated by Coco/R.
This was done to support sharing of the Coco/R .frame files with Spec#.
|
|
|
|
| |
Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
|
| |
|
| |
|
|
|
|
|
| |
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.
|
|
|
|
| |
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.
|