From 9fccb9dc8ea59b88970f2a3714b8b5d333ca5723 Mon Sep 17 00:00:00 2001
From: Yaakov <yaakov.smith@wisetechglobal.com>
Date: Thu, 19 Nov 2015 13:39:30 +1100
Subject: [PATCH] Extend postcondition on Path.GetTempFileName

Extends postcondition to not-null or whitespace, and
length >= 4 since it must end with ".TMP"
---
 Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs b/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs
index b5e22c54..b6bb5b45 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs
@@ -216,7 +216,8 @@ public static string GetRandomFileName()
 
     public static string GetTempFileName()
     {
-      Contract.Ensures(Contract.Result<string>() != null);
+      Contract.Ensures(!string.IsNullOrWhitespace(Contract.Result<string>()));
+      Contract.Ensures(Contract.Result<string>().Length >= 4);
       Contract.EnsuresOnThrow<System.IO.IOException>(true, @"An I/O error occurs, such as no unique temporary file name is available. - or - This method was unable to create a temporary file.");
       return default(string);
     }