diff options
| author |  wuestholz <unknown> | 2011-09-23 15:09:38 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-09-23 15:09:38 +0200 |
| commit | ffbb1cab70a1fcc8ba2d205cb652d3a65f566672 (patch) | |
| tree | e13057bbd38f28cb8c0fab6ce9c50031228d714f /Dafny | |
| parent | 578d587dd67fa04a9f797a619e690b058c975e76 (diff) | |
Dafny: Added some assertions.
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Compiler.cs | 5 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 6a448172..902c1f1c 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -27,7 +27,10 @@ namespace Microsoft.Dafny { TextWriter wr;
public int ErrorCount;
- void Error(string msg, params object[] args) {Contract.Requires(msg != null);
+ void Error(string msg, params object[] args) {
+ Contract.Requires(msg != null);
+ Contract.Requires(args != null);
+
string s = string.Format("Compilation error: " + msg, args);
Console.WriteLine(s);
wr.WriteLine("/* {0} */", s);
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 0a553036..1a0c97de 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -315,7 +315,7 @@ namespace Microsoft.Dafny { public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
- Contract.Requires(typeArgs != null);
+ Contract.Requires(cce.NonNullElements(typeArgs));
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
|