Added the option to let user determine whether or not GPUVerify should add invariants checking equality between arrays.

2 files changed, 9 insertions, 3 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index f2842d8f..f17efffe 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -16,8 +16,9 @@ namespace GPUVerify
         public static string outputFile = null;

 

         public static bool OnlyDivergence = false;

-        public static bool FullAbstraction;

-        public static bool Inference;

+        public static bool FullAbstraction = false;

+        public static bool Inference = false;

+        public static bool ArrayEqualities = false;

         public static string invariantsFile = null;

         public static bool DividedArray = false;

         public static string ArrayToCheck = null;

@@ -129,6 +130,11 @@ namespace GPUVerify
 

                     break;

 

+                    case "-arrayEqualities":

+                    case "/arrayEqualities":

+                    ArrayEqualities = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 662e2578..ed552598 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -918,7 +918,7 @@ namespace GPUVerify
                     }

                 }

 

-                if (!CommandLineOptions.FullAbstraction)

+                if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)

                 {

                     foreach (Variable v in NonLocalState.getAllNonLocalVariables())

                     {