diff options
| author |  Ally Donaldson <unknown> | 2015-01-22 09:19:50 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2015-01-22 09:19:50 +0000 |
| commit | 22ec7485362d7da6e19cab411d0805f4f128acc8 (patch) | |
| tree | de7b38761bebe40573ce4684a26c6a3c46e8a04a /Source | |
| parent | 033f25a8791a36b74925033368fcea946a2290de (diff) | |
| parent | 214b1a07c44d10eac99200147fe46e57a0297513 (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 47 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 3 |
2 files changed, 48 insertions, 2 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 13356aff..f2b2c0ca 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -213,6 +213,52 @@ namespace Microsoft.Boogie }
}
+ public class LayerEraser : ReadOnlyVisitor
+ {
+ private QKeyValue RemoveLayerAttribute(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = RemoveLayerAttribute(iter.Next);
+ return (iter.Key == "layer") ? iter.Next : iter;
+ }
+
+ public override Variable VisitVariable(Variable node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitVariable(node);
+ }
+
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitProcedure(node);
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitImplementation(node);
+ }
+
+ public override Requires VisitRequires(Requires node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitRequires(node);
+ }
+
+ public override Ensures VisitEnsures(Ensures node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitEnsures(node);
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitAssertCmd(node);
+ }
+ }
+
public class MoverTypeChecker : ReadOnlyVisitor
{
CheckingContext checkingContext;
@@ -427,6 +473,7 @@ namespace Microsoft.Boogie this.VisitProgram(program);
if (errorCount > 0) return;
YieldTypeChecker.PerformYieldSafeCheck(this);
+ new LayerEraser().VisitProgram(program);
}
public IEnumerable<Variable> SharedVariables
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 90da808a..c0d66720 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -509,8 +509,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
Concurrency.Transform(linearTypeChecker, moverTypeChecker);
- var eraser = new LinearEraser();
- eraser.VisitProgram(program);
+ (new LinearEraser()).VisitProgram(program);
if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
{
int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
|