diff options
| author |  Unknown <afd@afd-THINK.hsd1.or.comcast.net.> | 2012-03-17 08:45:49 -0700 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.hsd1.or.comcast.net.> | 2012-03-17 08:45:49 -0700 |
| commit | f9fd0a289f17229e281ee5afc985ae7b479be677 (patch) | |
| tree | aabcd78f8b5462d883d53d5dfad3f937fcc899ee /Source/GPUVerify/GPUVerifier.cs | |
| parent | 42c6da4d57fd24a1a5ef01a6b2fab75effe2c91f (diff) | |
Improved kernel precondition generation
Diffstat (limited to 'Source/GPUVerify/GPUVerifier.cs')
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 86938ab2..662e2578 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1201,6 +1201,15 @@ namespace GPUVerify {
RaceInstrumenter.AddNoRaceContract(Proc);
}
+ else
+ {
+ for (int i = 0; i < Proc.InParams.Length / 2; i++)
+ {
+ 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]))));
+ }
+ }
}
}
|