diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-03-30 13:29:03 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-03-30 13:29:03 +0100 |
| commit | cca2c779e500f36ce74367ad3349d2fa73da43f7 (patch) | |
| tree | cbd47e05ad7f13ea09f6a5df968026934ade401d | |
| parent | 78045c2455af0730fa1eaebda291738d71483c1f (diff) | |
Fixed bug with GPUVerify precondition generation
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index d759e31e..c0987296 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1092,11 +1092,27 @@ namespace GPUVerify }
else
{
- for (int i = 0; i < Proc.InParams.Length / 2; i++)
+ bool foundNonUniform = false;
+ int indexOfFirstNonUniformParameter;
+ for (indexOfFirstNonUniformParameter = 0; indexOfFirstNonUniformParameter < Proc.InParams.Length; indexOfFirstNonUniformParameter++)
{
- Proc.Requires.Add(new Requires(false,
- Expr.Eq(new IdentifierExpr(Proc.InParams[i].tok, Proc.InParams[i]),
- new IdentifierExpr(Proc.InParams[i + Proc.InParams.Length / 2].tok, Proc.InParams[i + Proc.InParams.Length / 2]))));
+ if (!uniformityAnalyser.IsUniform(Proc.Name, StripThreadIdentifier(Proc.InParams[indexOfFirstNonUniformParameter].Name)))
+ {
+ foundNonUniform = true;
+ break;
+ }
+ }
+
+ if (foundNonUniform)
+ {
+ // I have a feeling this will never be reachable!!!
+ int numberOfNonUniformParameters = (Proc.InParams.Length - indexOfFirstNonUniformParameter) / 2;
+ for (int i = indexOfFirstNonUniformParameter; i < numberOfNonUniformParameters; i++)
+ {
+ Proc.Requires.Add(new Requires(false,
+ Expr.Eq(new IdentifierExpr(Proc.InParams[i].tok, Proc.InParams[i]),
+ new IdentifierExpr(Proc.InParams[i + numberOfNonUniformParameters].tok, Proc.InParams[i + numberOfNonUniformParameters]))));
+ }
}
}
|