diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-03-04 10:35:07 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-03-04 10:35:07 +0000 |
| commit | f5b0c348d36d771851208b7a744e94e909a3894c (patch) | |
| tree | c3180577ecc16f781767772d646f24e33e689ef1 /Source/GPUVerify/GPUVerifier.cs | |
| parent | a3527ac1ae5caf2c1d44b599ebf46fbd802e7ab9 (diff) | |
More annotation support
Diffstat (limited to 'Source/GPUVerify/GPUVerifier.cs')
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 632777c9..b4a5aa8f 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -438,6 +438,26 @@ namespace GPUVerify private void ProcessAccessInvariants(BigBlock bb)
{
+ CmdSeq newCommands = new CmdSeq();
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is AssertCmd)
+ {
+ newCommands.Add(new AssertCmd(c.tok, new AccessInvariantProcessor().VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));
+ }
+ else if (c is AssumeCmd)
+ {
+ newCommands.Add(new AssumeCmd(c.tok, new AccessInvariantProcessor().VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));
+ }
+ else
+ {
+ newCommands.Add(c);
+ }
+ }
+
+ bb.simpleCmds = newCommands;
+
if (bb.ec is WhileCmd)
{
WhileCmd whileCmd = bb.ec as WhileCmd;
@@ -2314,7 +2334,7 @@ namespace GPUVerify else if (c is AssertCmd)
{
AssertCmd ass = c as AssertCmd;
- if (HalfDualise)
+ if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
{
result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr)));
}
@@ -2326,7 +2346,7 @@ namespace GPUVerify else if (c is AssumeCmd)
{
AssumeCmd ass = c as AssumeCmd;
- if (HalfDualise)
+ if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
{
result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr)));
}
|