Added generation of invariants to restrict source location to sensible values.

Refactored Make...Variable() and FindOrCreate...Variable() functions to take
a variable name as a parameter rather than the variable itself.

1 files changed, 12 insertions, 5 deletions

diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
index b2710054..4374a0cc 100644
--- a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
+++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
@@ -615,15 +615,22 @@ namespace Microsoft.Boogie
       {

         foreach (Cmd c in b.Cmds)

         {

-          if (c.ToString().Contains(AccessType + "_SOURCE_")) 

+          if (b.tok.val.Equals("_LOG_" + AccessType) && c.ToString().Contains(AccessType + "_SOURCE_")) 

           {

             sourceVarName = Regex.Split(c.ToString(), " ")[1];

           }

         }

       }

-      sourceLocLineNo = error.Model.TryGetFunc(sourceVarName).GetConstant().AsInt();

-

-      if (sourceLocLineNo != 0)

+      if (sourceVarName != null)

+      {

+        Model.Func f = error.Model.TryGetFunc(sourceVarName);

+        if (f != null)

+        {

+          sourceLocLineNo = f.GetConstant().AsInt();

+        }

+      }

+      

+      if (sourceLocLineNo != 0 && sourceLocLineNo != -1)

       {

         while ((fileLine = tr.ReadLine()) != null)

         {

@@ -651,7 +658,7 @@ namespace Microsoft.Boogie
       }

       else

       {

-        Console.WriteLine("sourceLocLineNo is 0. No sourceloc at that location.\n");

+        Console.WriteLine("sourceLocLineNo is {0}. No sourceloc at that location.\n", sourceLocLineNo);

         return null;

       } 

       tr.Close();