diff options
| -rw-r--r-- | Source/Core/Absy.cs | 22 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 3 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 |
3 files changed, 20 insertions, 7 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 30333259..d5abda9b 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -446,10 +446,16 @@ namespace Microsoft.Boogie { public IEnumerable<Declaration> TopLevelDeclarations
{
- get
- {
- return topLevelDeclarations;
- }
+ get
+ {
+ return topLevelDeclarations;
+ }
+
+ set
+ {
+ ClearTopLevelDeclarations();
+ AddTopLevelDeclarations(value);
+ }
}
public void AddTopLevelDeclaration(Declaration decl)
@@ -468,6 +474,14 @@ namespace Microsoft.Boogie { this.globalVariablesCache = null;
}
+ public void RemoveTopLevelDeclaration(Declaration decl)
+ {
+ Contract.Requires(!TopLevelDeclarationsAreFrozen);
+
+ topLevelDeclarations.Remove(decl);
+ this.globalVariablesCache = null;
+ }
+
public void RemoveTopLevelDeclarations(Predicate<Declaration> match)
{
Contract.Requires(!TopLevelDeclarationsAreFrozen);
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 6920ade3..cc8298b3 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -2401,8 +2401,7 @@ namespace Microsoft.Boogie.Houdini { var decls = new List<Declaration>(copy.Values);
decls.AddRange(program.TopLevelDeclarations.Where(decl => !(decl is Implementation)));
- program.ClearTopLevelDeclarations();
- program.AddTopLevelDeclarations(decls);
+ program.TopLevelDeclarations = decls;
var name2Proc = new Dictionary<string, Procedure>();
foreach (var proc in program.Procedures)
{
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index e8194891..5d01f2c1 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2144,7 +2144,7 @@ namespace VC { protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg) {
var ret = new HashSet<VCExprVar>();
- results.ForEach(s => ret.UnionWith(s));
+ results.Iter(s => ret.UnionWith(s));
return ret;
}
}
|