Uniformity analysis. Patch by Peter Collingbourne.

1 files changed, 67 insertions, 62 deletions

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index 60c28b5b..fae08aa3 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -1,62 +1,67 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    class NullRaceInstrumenter : IRaceInstrumenter

-    {

-

-        public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)

-        {

-            

-        }

-

-        public void AddKernelPrecondition()

-        {

-            

-        }

-

-        public void AddRaceCheckingInstrumentation()

-        {

-

-        }

-

-        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)

-        {

-            return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);

-        }

-

-        public void AddRaceCheckingCandidateRequires(Procedure Proc)

-        {

-

-        }

-

-        public void AddRaceCheckingCandidateEnsures(Procedure Proc)

-        {

-

-        }

-

-        public void AddRaceCheckingDeclarations()

-        {

-

-        }

-        

-        public void AddSourceLocationLoopInvariants(Implementation impl, IRegion region)

-        {

-

-        }

-

-        public void AddStandardSourceVariablePreconditions()

-        {

-

-        }

-

-        public void AddStandardSourceVariablePostconditions()

-        {

-

-        }

-    }

-}

+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+    class NullRaceInstrumenter : IRaceInstrumenter
+    {
+
+        public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)
+        {
+            
+        }
+
+        public void AddKernelPrecondition()
+        {
+            
+        }
+
+        public void AddRaceCheckingInstrumentation()
+        {
+
+        }
+
+        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
+        {
+            return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
+        }
+
+        public void AddRaceCheckingCandidateRequires(Procedure Proc)
+        {
+
+        }
+
+        public void AddRaceCheckingCandidateEnsures(Procedure Proc)
+        {
+
+        }
+
+        public void AddRaceCheckingDeclarations()
+        {
+
+        }
+        
+        public void AddSourceLocationLoopInvariants(Implementation impl, IRegion region)
+        {
+
+        }
+
+        public void DoHoudiniPointerAnalysis(Procedure Proc)
+        {
+
+        }
+
+        public void AddStandardSourceVariablePreconditions()
+        {
+
+        }
+
+        public void AddStandardSourceVariablePostconditions()
+        {
+
+        }
+    }
+}