diff options
| -rw-r--r-- | Source/Concurrency/LinearSets.cs | 12 | ||||
| -rw-r--r-- | Source/Concurrency/Program.cs | 4 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 51 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 26 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 4 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 19 | ||||
| -rw-r--r-- | Source/Core/Scanner.cs | 9 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 7 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 11 | ||||
| -rw-r--r-- | Source/Houdini/CandidateDependenceAnalyser.cs | 4 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 2 |
13 files changed, 95 insertions, 58 deletions
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index b6e23e38..e3bc3bfe 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -779,14 +779,14 @@ namespace Microsoft.Boogie foreach (LinearDomain domain in linearDomains.Values)
{
- program.TopLevelDeclarations.Add(domain.mapConstBool);
- program.TopLevelDeclarations.Add(domain.mapConstInt);
- program.TopLevelDeclarations.Add(domain.mapEqInt);
- program.TopLevelDeclarations.Add(domain.mapImpBool);
- program.TopLevelDeclarations.Add(domain.mapOrBool);
+ program.AddTopLevelDeclaration(domain.mapConstBool);
+ program.AddTopLevelDeclaration(domain.mapConstInt);
+ program.AddTopLevelDeclaration(domain.mapEqInt);
+ program.AddTopLevelDeclaration(domain.mapImpBool);
+ program.AddTopLevelDeclaration(domain.mapOrBool);
foreach (Axiom axiom in domain.axioms)
{
- program.TopLevelDeclarations.Add(axiom);
+ program.AddTopLevelDeclaration(axiom);
}
}
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index 915eadda..562044a9 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -36,8 +36,8 @@ namespace Microsoft.Boogie {
decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
}
- program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));
- program.TopLevelDeclarations.AddRange(decls);
+ program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x));
+ program.AddTopLevelDeclarations(decls);
}
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index baefd09a..38a83b12 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -296,7 +296,36 @@ namespace Microsoft.Boogie { public class Program : Absy {
[Rep]
- public List<Declaration/*!*/>/*!*/ TopLevelDeclarations;
+ private List<Declaration/*!*/>/*!*/ topLevelDeclarations;
+
+ public IEnumerable<Declaration> TopLevelDeclarations
+ {
+ get
+ {
+ return topLevelDeclarations;
+ }
+ }
+
+ public void AddTopLevelDeclaration(Declaration decl)
+ {
+ topLevelDeclarations.Add(decl);
+ }
+
+ public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)
+ {
+ topLevelDeclarations.AddRange(decls);
+ }
+
+ public void RemoveTopLevelDeclarations(Predicate<Declaration> match)
+ {
+ topLevelDeclarations.RemoveAll(match);
+ }
+
+ public void ClearTopLevelDeclarations()
+ {
+ topLevelDeclarations.Clear();
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));
@@ -306,13 +335,13 @@ namespace Microsoft.Boogie { public Program()
: base(Token.NoToken) {
- this.TopLevelDeclarations = new List<Declaration>();
+ this.topLevelDeclarations = new List<Declaration>();
}
public void Emit(TokenTextWriter stream) {
Contract.Requires(stream != null);
stream.SetToken(this);
- this.TopLevelDeclarations.Emit(stream);
+ this.topLevelDeclarations.Emit(stream);
}
public void ProcessDatatypeConstructors() {
@@ -329,17 +358,18 @@ namespace Microsoft.Boogie { constructors.Add(func.Name, constructor);
prunedTopLevelDeclarations.Add(constructor);
}
- TopLevelDeclarations = prunedTopLevelDeclarations;
+ ClearTopLevelDeclarations();
+ AddTopLevelDeclarations(prunedTopLevelDeclarations);
foreach (DatatypeConstructor f in constructors.Values) {
for (int i = 0; i < f.InParams.Count; i++) {
DatatypeSelector selector = new DatatypeSelector(f, i);
f.selectors.Add(selector);
- TopLevelDeclarations.Add(selector);
+ AddTopLevelDeclaration(selector);
}
DatatypeMembership membership = new DatatypeMembership(f);
f.membership = membership;
- TopLevelDeclarations.Add(membership);
+ AddTopLevelDeclaration(membership);
}
}
@@ -385,7 +415,8 @@ namespace Microsoft.Boogie { }
prunedTopLevelDecls.Add(d);
}
- TopLevelDeclarations = prunedTopLevelDecls;
+ ClearTopLevelDeclarations();
+ AddTopLevelDeclarations(prunedTopLevelDecls);
foreach (var v in Variables) {
v.ResolveWhere(rc);
@@ -1067,8 +1098,8 @@ namespace Microsoft.Boogie { foreach (Implementation/*!*/ loopImpl in loopImpls)
{
Contract.Assert(loopImpl != null);
- TopLevelDeclarations.Add(loopImpl);
- TopLevelDeclarations.Add(loopImpl.Proc);
+ AddTopLevelDeclaration(loopImpl);
+ AddTopLevelDeclaration(loopImpl.Proc);
}
return fullMap;
}
@@ -1098,7 +1129,7 @@ namespace Microsoft.Boogie { invariantGenerationCounter++;
ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) });
- TopLevelDeclarations.Add(ExistentialBooleanConstant);
+ AddTopLevelDeclaration(ExistentialBooleanConstant);
return ExistentialBooleanConstant;
}
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index e954944f..644a5d3d 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -31,7 +31,7 @@ readonly StructuredCmd/*!*/ dummyStructuredCmd; ///Returns the number of parsing errors encountered. If 0, "program" returns as
///the parsed program.
///</summary>
-public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(defines,true));
@@ -41,25 +41,25 @@ public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> if (filename == "stdin.bpl") {
var s = ParserHelper.Fill(Console.In, defines);
- return Parse(s, filename, out program);
+ return Parse(s, filename, out program, useBaseName);
} else {
FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
var s = ParserHelper.Fill(stream, defines);
- var ret = Parse(s, filename, out program);
+ var ret = Parse(s, filename, out program, useBaseName);
stream.Close();
return ret;
}
}
-public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
Contract.Requires(s != null);
Contract.Requires(filename != null);
byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
- Scanner scanner = new Scanner(ms, errors, filename);
+ Scanner scanner = new Scanner(ms, errors, filename, useBaseName);
Parser parser = new Parser(scanner, errors, false);
parser.Parse();
@@ -168,31 +168,31 @@ BoogiePL .)
{ Consts<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
- Pgm.TopLevelDeclarations.Add(v);
+ Pgm.AddTopLevelDeclaration(v);
}
.)
| Function<out ds> (. foreach(Bpl.Declaration/*!*/ d in ds){
Contract.Assert(d != null);
- Pgm.TopLevelDeclarations.Add(d);
+ Pgm.AddTopLevelDeclaration(d);
}
.)
- | Axiom<out ax> (. Pgm.TopLevelDeclarations.Add(ax); .)
+ | Axiom<out ax> (. Pgm.AddTopLevelDeclaration(ax); .)
| UserDefinedTypes<out ts> (. foreach(Declaration/*!*/ td in ts){
Contract.Assert(td != null);
- Pgm.TopLevelDeclarations.Add(td);
+ Pgm.AddTopLevelDeclaration(td);
}
.)
| GlobalVars<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
- Pgm.TopLevelDeclarations.Add(v);
+ Pgm.AddTopLevelDeclaration(v);
}
.)
- | Procedure<out pr, out im> (. Pgm.TopLevelDeclarations.Add(pr);
+ | Procedure<out pr, out im> (. Pgm.AddTopLevelDeclaration(pr);
if (im != null) {
- Pgm.TopLevelDeclarations.Add(im);
+ Pgm.AddTopLevelDeclaration(im);
}
.)
- | Implementation<out nnim> (. Pgm.TopLevelDeclarations.Add(nnim); .)
+ | Implementation<out nnim> (. Pgm.AddTopLevelDeclaration(nnim); .)
}
EOF
.
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 45c68fdd..603f7e72 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -44,10 +44,10 @@ namespace Microsoft.Boogie { Desugar(prog, out axioms, out functions);
foreach (var f in functions) {
- prog.TopLevelDeclarations.Add(f);
+ prog.AddTopLevelDeclaration(f);
}
foreach (var a in axioms) {
- prog.TopLevelDeclarations.Add(new Axiom(a.tok, a));
+ prog.AddTopLevelDeclaration(new Axiom(a.tok, a));
}
}
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 2149e12c..25be7f27 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -12,6 +12,8 @@ using Bpl = Microsoft.Boogie; using System;
using System.Diagnostics.Contracts;
+namespace Microsoft.Boogie {
+
public class Parser {
@@ -218,7 +220,7 @@ private class BvBounds : Expr { Consts(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
- Pgm.TopLevelDeclarations.Add(v);
+ Pgm.AddTopLevelDeclaration(v);
}
break;
@@ -227,21 +229,21 @@ private class BvBounds : Expr { Function(out ds);
foreach(Bpl.Declaration/*!*/ d in ds){
Contract.Assert(d != null);
- Pgm.TopLevelDeclarations.Add(d);
+ Pgm.AddTopLevelDeclaration(d);
}
break;
}
case 29: {
Axiom(out ax);
- Pgm.TopLevelDeclarations.Add(ax);
+ Pgm.AddTopLevelDeclaration(ax);
break;
}
case 30: {
UserDefinedTypes(out ts);
foreach(Declaration/*!*/ td in ts){
Contract.Assert(td != null);
- Pgm.TopLevelDeclarations.Add(td);
+ Pgm.AddTopLevelDeclaration(td);
}
break;
@@ -250,23 +252,23 @@ private class BvBounds : Expr { GlobalVars(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
- Pgm.TopLevelDeclarations.Add(v);
+ Pgm.AddTopLevelDeclaration(v);
}
break;
}
case 32: {
Procedure(out pr, out im);
- Pgm.TopLevelDeclarations.Add(pr);
+ Pgm.AddTopLevelDeclaration(pr);
if (im != null) {
- Pgm.TopLevelDeclarations.Add(im);
+ Pgm.AddTopLevelDeclaration(im);
}
break;
}
case 33: {
Implementation(out nnim);
- Pgm.TopLevelDeclarations.Add(nnim);
+ Pgm.AddTopLevelDeclaration(nnim);
break;
}
}
@@ -2286,3 +2288,4 @@ public class FatalError: Exception { }
+}
\ No newline at end of file diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index b050fcdd..5b5c0306 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -8,7 +8,7 @@ using System.Diagnostics.Contracts; using Microsoft.Boogie;
-
+namespace Microsoft.Boogie {
//-----------------------------------------------------------------------------------
// Buffer
@@ -296,7 +296,7 @@ public class Scanner { }
// [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName) : base() {
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -313,7 +313,7 @@ public class Scanner { }
// [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName) : base() {
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -325,7 +325,7 @@ public class Scanner { Init();
}
- private string GetBaseName(string fileName) {
+ string GetBaseName(string fileName) {
return System.IO.Path.GetFileName(fileName); // Return basename
}
@@ -807,3 +807,4 @@ public class Scanner { public delegate void ErrorProc(int n, string filename, int line, int col);
+}
\ No newline at end of file diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index d4be8ed4..3f3ad5ae 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -9,6 +9,7 @@ using System.Collections.Generic;
using System.Diagnostics.Contracts;
+using System.Linq;
namespace Microsoft.Boogie {
[ContractClass(typeof(VisitorContracts))]
@@ -429,7 +430,9 @@ namespace Microsoft.Boogie { public virtual Program VisitProgram(Program node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Program>() != null);
- node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
+ var decls = node.TopLevelDeclarations.ToList();
+ node.ClearTopLevelDeclarations();
+ node.AddTopLevelDeclarations(this.VisitDeclarationList(decls));
return node;
}
public virtual QKeyValue VisitQKeyValue(QKeyValue node) {
@@ -979,7 +982,7 @@ namespace Microsoft.Boogie { public override Program VisitProgram(Program node)
{
Contract.Ensures(Contract.Result<Program>() == node);
- this.VisitDeclarationList(node.TopLevelDeclarations);
+ this.VisitDeclarationList(node.TopLevelDeclarations.ToList());
return node;
}
public override QKeyValue VisitQKeyValue(QKeyValue node) {
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 093f1d90..11558750 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -642,7 +642,7 @@ namespace Microsoft.Boogie }
else if (programSnippet != null)
{
- program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);
+ program.AddTopLevelDeclarations(programSnippet.TopLevelDeclarations);
}
}
if (!okay)
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index e268a8d7..d9961a64 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -2399,11 +2399,10 @@ namespace Microsoft.Boogie.Houdini { proc.Ensures = nensures;
}
- var decls = new List<Declaration>();
- copy.Values.Iter(impl => decls.Add(impl));
- program.TopLevelDeclarations.Where(decl => !(decl is Implementation))
- .Iter(decl => decls.Add(decl));
- program.TopLevelDeclarations = decls;
+ var decls = new List<Declaration>(copy.Values);
+ decls.AddRange(program.TopLevelDeclarations.Where(decl => !(decl is Implementation)));
+ program.ClearTopLevelDeclarations();
+ program.AddTopLevelDeclarations(decls);
var name2Proc = new Dictionary<string, Procedure>();
foreach (var proc in program.Procedures)
{
@@ -3261,7 +3260,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl));
+ program.RemoveTopLevelDeclarations(decl => tempP.Contains(decl));
var upperPreds = new Dictionary<string, List<Expr>>();
foreach (var impl in program.Implementations)
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 9ff333dc..12bad0ac 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -396,14 +396,14 @@ namespace Microsoft.Boogie.Houdini { new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_active", Type.Bool),
false);
stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });
- prog.TopLevelDeclarations.Add(stageActive);
+ prog.AddTopLevelDeclaration(stageActive);
stageToActiveBoolean[stage.GetId()] = stageActive;
var stageComplete = new Constant(Token.NoToken,
new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_complete", Type.Bool),
false);
stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });
- prog.TopLevelDeclarations.Add(stageComplete);
+ prog.AddTopLevelDeclaration(stageComplete);
stageToCompleteBoolean[stage.GetId()] = stageComplete;
}
#endregion
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 6b1f2c39..74cf0d26 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -1244,7 +1244,7 @@ namespace Microsoft.Boogie.Houdini { }
// Remove the existential constants
- prog.TopLevelDeclarations.RemoveAll(item => (item is Variable) &&
+ prog.RemoveTopLevelDeclarations(item => (item is Variable) &&
(houdiniConstants.Select(c => c.Name).Contains((item as Variable).Name)));
}
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 04b976ea..ee33253f 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -548,7 +548,7 @@ namespace Microsoft.Boogie {
Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type));
interfaceVarCopies[i].Add(constant);
- //program.TopLevelDeclarations.Add(constant);
+ //program.AddTopLevelDeclaration(constant);
}
}
}
|