diff options
| author |  Peter Collingbourne <peter@pcc.me.uk> | 2012-05-31 20:20:42 +0100 |
|---|---|---|
| committer | Peter Collingbourne <peter@pcc.me.uk> | 2012-05-31 20:20:42 +0100 |
| commit | 3a1932a46ac936d80ba87916f38d4450f55adc48 (patch) | |
| tree | da074b97b796457116dcbaa7f02f2df5a2072893 /Source/GPUVerify | |
| parent | 486b849f4eade583dd12f7151311375112aa87e4 (diff) | |
GPUVerify: resolve barrier implementation in unstructured mode
Resolution of goto labels is required for the graph
builder to work.
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 27ec052e..4e30951e 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1403,6 +1403,9 @@ namespace GPUVerify StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);
Implementation BarrierImplementation = new Implementation(BarrierProcedure.tok, BarrierProcedure.Name, new TypeVariableSeq(), BarrierProcedure.InParams, BarrierProcedure.OutParams, new VariableSeq(), statements);
+ if (CommandLineOptions.Unstructured)
+ BarrierImplementation.Resolve(ResContext);
+
BarrierImplementation.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });
BarrierProcedure.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });
|