diff options
author | Rustan Leino <unknown> | 2016-02-29 15:31:30 -0800 |
---|---|---|
committer | Rustan Leino <unknown> | 2016-02-29 15:31:30 -0800 |
commit | 9f4d81cb7056501547a5116796a3112da8054433 (patch) | |
tree | 209590d4472b8faf635d727a8f6b9bd8633da9b4 | |
parent | 0531b8772f4174d807caecc356ecaa41adca8c8c (diff) |
Added a return-value contract
-rw-r--r-- | Source/Dafny/Translator.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 940bb328..1700198f 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7040,6 +7040,7 @@ namespace Microsoft.Dafny { {
Contract.Requires(tok != null);
Contract.Requires(condition != null);
+ Contract.Ensures(Contract.Result<Bpl.Requires>() != null);
Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment);
if (errorMessage != null) {
req.ErrorData = errorMessage;
|