Made invariant of class 'Program' robust by

-adding various preconditions
-removing null elements in the setter
-using the "ReadOnlyList" wrapper.

1 files changed, 9 insertions, 3 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 4f743910..9a17f50b 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -308,7 +308,7 @@ namespace Microsoft.Boogie {
 

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));

+      Contract.Invariant(cce.NonNullElements(this.topLevelDeclarations));

       Contract.Invariant(globalVariablesCache == null || cce.NonNullElements(globalVariablesCache));

     }

     

@@ -466,17 +466,21 @@ namespace Microsoft.Boogie {
     {

         get

         {

-            return topLevelDeclarations;

+            Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Declaration>>()));

+            return topLevelDeclarations.AsReadOnly();

         }

 

         set

         {

+            Contract.Requires(value != null);

             // materialize the decls, in case there is any dependency 

             // back on topLevelDeclarations

             var v = value.ToList();

+            // remove null elements

+            v.RemoveAll(d => (d == null));

             // now clear the decls

             ClearTopLevelDeclarations();

-            // and add the value

+            // and add the values

             AddTopLevelDeclarations(v);

         }

     }

@@ -484,6 +488,7 @@ namespace Microsoft.Boogie {
     public void AddTopLevelDeclaration(Declaration decl)

     {

       Contract.Requires(!TopLevelDeclarationsAreFrozen);

+      Contract.Requires(decl != null);

 

       topLevelDeclarations.Add(decl);

       this.globalVariablesCache = null;

@@ -492,6 +497,7 @@ namespace Microsoft.Boogie {
     public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)

     {

       Contract.Requires(!TopLevelDeclarationsAreFrozen);

+      Contract.Requires(cce.NonNullElements(decls));

 

       topLevelDeclarations.AddRange(decls);

       this.globalVariablesCache = null;