diff options
| author |  Unknown <afd@afd-THINK> | 2011-11-16 11:52:27 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK> | 2011-11-16 11:52:27 +0000 |
| commit | d017f7a654d8d9716a4fa64a547663a1e34eb8d3 (patch) | |
| tree | 664d5fb1a1f1e637739a662577ddb4f0c7da5d9b /Source/GPUVerify | |
| parent | 8e1a19a4fc73dcde12f0d20d3f40fc5fb0146425 (diff) | |
Better support for race-checking contracts
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 5 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 23 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 15 |
3 files changed, 40 insertions, 3 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 2f08477b..bef0505e 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -20,6 +20,7 @@ namespace GPUVerify public static bool Inference;
public static string invariantsFile = null;
public static bool DividedArray = false;
+ public static string ArrayToCheck = null;
public static bool DividedAccesses = false;
public static bool Eager = false;
@@ -77,6 +78,10 @@ namespace GPUVerify case "-dividedArray":
case "/dividedArray":
+ if (hasColonArgument)
+ {
+ ArrayToCheck = afterColon;
+ }
DividedArray = true;
break;
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 36881f88..c15327ca 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -414,7 +414,6 @@ namespace GPUVerify private void ComputeInvariant()
{
- List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants();
invariantGenerationCounter = 0;
@@ -430,6 +429,8 @@ namespace GPUVerify continue;
}
+ List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants(Impl.Name);
+
HashSet<string> LocalNames = new HashSet<string>();
foreach (Variable v in Impl.LocVars)
{
@@ -613,7 +614,7 @@ namespace GPUVerify Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
- private List<Expr> GetUserSuppliedInvariants()
+ private List<Expr> GetUserSuppliedInvariants(string ProcedureName)
{
List<Expr> result = new List<Expr>();
@@ -627,6 +628,24 @@ namespace GPUVerify int lineNumber = 1;
while ((line = sr.ReadLine()) != null)
{
+ string[] components = line.Split(':');
+
+ if (components.Length != 1 && components.Length != 2)
+ {
+ Console.WriteLine("Ignoring badly formed candidate invariant '" + line + "' at '" + CommandLineOptions.invariantsFile + "' line " + lineNumber);
+ continue;
+ }
+
+ if (components.Length == 2)
+ {
+ if (!components[0].Trim().Equals(ProcedureName))
+ {
+ continue;
+ }
+
+ line = components[1];
+ }
+
string temp_program_text = "axiom (" + line + ");";
TokenTextWriter writer = new TokenTextWriter("temp_out.bpl");
writer.WriteLine(temp_program_text);
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 9791d6cf..9fb01ee1 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -134,6 +134,8 @@ namespace GPUVerify if (CommandLineOptions.DividedArray)
{
+ bool FoundArray = CommandLineOptions.ArrayToCheck == null;
+
foreach (Variable v in g.NonLocalState.getAllNonLocalVariables())
{
if (CommandLineOptions.DividedAccesses)
@@ -163,9 +165,20 @@ namespace GPUVerify }
else
{
- doit("temp_" + v.Name + ".bpl", v, -1, -1);
+ if (CommandLineOptions.ArrayToCheck == null || CommandLineOptions.ArrayToCheck.Equals(v.Name))
+ {
+ FoundArray = true;
+ doit("temp_" + v.Name, v, -1, -1);
+ }
}
}
+
+ if (!FoundArray)
+ {
+ Console.WriteLine("Did not find a non-local array named " + CommandLineOptions.ArrayToCheck);
+ Environment.Exit(1);
+ }
+
}
else
{
|