From d017f7a654d8d9716a4fa64a547663a1e34eb8d3 Mon Sep 17 00:00:00 2001
From: Unknown <afd@afd-THINK>
Date: Wed, 16 Nov 2011 11:52:27 +0000
Subject: Better support for race-checking contracts

---
 Source/GPUVerify/GPUVerifier.cs | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

(limited to 'Source/GPUVerify/GPUVerifier.cs')

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 36881f88..c15327ca 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -414,7 +414,6 @@ namespace GPUVerify
 
         private void ComputeInvariant()
         {
-            List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants();
 
             invariantGenerationCounter = 0;
 
@@ -430,6 +429,8 @@ namespace GPUVerify
                         continue;
                     }
 
+                    List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants(Impl.Name);
+
                     HashSet<string> LocalNames = new HashSet<string>();
                     foreach (Variable v in Impl.LocVars)
                     {
@@ -613,7 +614,7 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
         }
 
-        private List<Expr> GetUserSuppliedInvariants()
+        private List<Expr> GetUserSuppliedInvariants(string ProcedureName)
         {
             List<Expr> result = new List<Expr>();
 
@@ -627,6 +628,24 @@ namespace GPUVerify
             int lineNumber = 1;
             while ((line = sr.ReadLine()) != null)
             {
+                string[] components = line.Split(':');
+
+                if (components.Length != 1 && components.Length != 2)
+                {
+                    Console.WriteLine("Ignoring badly formed candidate invariant '" + line + "' at '" + CommandLineOptions.invariantsFile + "' line " + lineNumber);
+                    continue;
+                }
+
+                if (components.Length == 2)
+                {
+                    if (!components[0].Trim().Equals(ProcedureName))
+                    {
+                        continue;
+                    }
+
+                    line = components[1];
+                }
+
                 string temp_program_text = "axiom (" + line + ");";
                 TokenTextWriter writer = new TokenTextWriter("temp_out.bpl");
                 writer.WriteLine(temp_program_text);
-- 
cgit v1.2.3