diff options
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify/Predicator.cs | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 8c090b6a..b2e54dbd 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -44,6 +44,8 @@ namespace GPUVerify public static bool ShowMayBeTidPlusConstantAnalysis = false;
public static bool ShowArrayControlFlowAnalysis = false;
+ public static bool NoLoopPredicateInvariants = false;
+
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -196,6 +198,11 @@ namespace GPUVerify ShowArrayControlFlowAnalysis = true;
break;
+ case "-noLoopPredicateInvariants":
+ case "/noLoopPredicateInvariants":
+ NoLoopPredicateInvariants = true;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs index 0950cd9a..316a3df6 100644 --- a/Source/GPUVerify/Predicator.cs +++ b/Source/GPUVerify/Predicator.cs @@ -251,7 +251,7 @@ namespace GPUVerify VisitWhileInvariants(whileCmd.Invariants, NewGuard),
VisitStmtList(whileCmd.Body));
- if (NewInvariant != null)
+ if (NewInvariant != null && !CommandLineOptions.NoLoopPredicateInvariants)
{
NewWhile.Invariants.Add(NewInvariant);
}
|