From 673869879ae1c3ec7a1797ccfdd66295b52188c0 Mon Sep 17 00:00:00 2001
From: Egor Kyshtymov <unknown>
Date: Tue, 28 Aug 2012 11:52:35 +0100
Subject: 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.

---
 Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'Source/GPUVerifyBoogieDriver')

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();
-- 
cgit v1.2.3