Uniformity analysis. Patch by Peter Collingbourne.

1 files changed, 31 insertions, 30 deletions

diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index 2e997fe0..c85989c9 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -1,30 +1,31 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    interface IRaceInstrumenter

-    {

-        void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region);

-        void AddKernelPrecondition();

-

-        void AddRaceCheckingInstrumentation();

-

-        void AddRaceCheckingDeclarations();

-

-        BigBlock MakeResetReadWriteSetStatements(Variable v, int thread);

-

-        void AddRaceCheckingCandidateRequires(Procedure Proc);

-

-        void AddRaceCheckingCandidateEnsures(Procedure Proc);

-

-        void AddSourceLocationLoopInvariants(Implementation impl, IRegion region);

-

-        void AddStandardSourceVariablePreconditions();

-

-        void AddStandardSourceVariablePostconditions();

-    }

-}

+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+    interface IRaceInstrumenter
+    {
+        void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region);
+        void AddKernelPrecondition();
+
+        void AddRaceCheckingInstrumentation();
+
+        void AddRaceCheckingDeclarations();
+
+        BigBlock MakeResetReadWriteSetStatements(Variable v, int thread);
+
+        void AddRaceCheckingCandidateRequires(Procedure Proc);
+
+        void AddRaceCheckingCandidateEnsures(Procedure Proc);
+
+        void AddSourceLocationLoopInvariants(Implementation impl, IRegion region);
+
+        void DoHoudiniPointerAnalysis(Procedure Proc);
+        void AddStandardSourceVariablePreconditions();
+
+        void AddStandardSourceVariablePostconditions();
+    }
+}