diff options
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 8 | ||||
| -rw-r--r-- | Source/GPUVerify/Predicator.cs | 2 |
4 files changed, 12 insertions, 9 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/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index b767816c..9881b0f0 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -152,10 +152,6 @@ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
- <ProjectReference Include="..\BoogieDriver\BoogieDriver.csproj">
- <Project>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</Project>
- <Name>BoogieDriver</Name>
- </ProjectReference>
<ProjectReference Include="..\Core\Core.csproj">
<Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index b70260ce..48cd8a2f 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -28,7 +28,7 @@ namespace GPUVerify if (CommandLineOptions.inputFiles.Count < 1)
{
- OnlyBoogie.ErrorWriteLine("*** Error: No input files were specified.");
+ Console.WriteLine("*** Error: No input files were specified.");
Environment.Exit(1);
}
@@ -41,7 +41,7 @@ namespace GPUVerify }
if (extension != ".gbpl")
{
- OnlyBoogie.AdvisoryWriteLine("Warning '{0}': Should only pass filename with extension .gbpl. Input must be GBoogie programs.", file);
+ Console.WriteLine("Warning '{0}': Should only pass filename with extension .gbpl. Input must be GBoogie programs.", file);
}
}
@@ -220,14 +220,14 @@ namespace GPUVerify errorCount = Parser.Parse(bplFileName, defines, out programSnippet);
if (programSnippet == null || errorCount != 0)
{
- OnlyBoogie.ErrorWriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
+ Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
okay = false;
continue;
}
}
catch (IOException e)
{
- OnlyBoogie.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
+ Console.WriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
okay = false;
continue;
}
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);
}
|