Add support for 'verified_under' attributes on procedure calls and invariants.

1 files changed, 14 insertions, 0 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b5581ea6..137e2363 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2656,6 +2656,13 @@ namespace Microsoft.Boogie {
             reqCopy.Condition = Substituter.Apply(s, req.Condition);

             AssertCmd/*!*/ a = new AssertRequiresCmd(this, reqCopy);

             Contract.Assert(a != null);

+            if (Attributes != null)

+            {

+              // Inherit attributes of call.

+              var attrCopy = (QKeyValue)cce.NonNull(Attributes.Clone());

+              attrCopy = Substituter.Apply(s, attrCopy);

+              a.Attributes = attrCopy;

+            }

             a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;

             newBlockBody.Add(a);

           }

@@ -2676,6 +2683,13 @@ namespace Microsoft.Boogie {
         Contract.Assert(expr != null);

         AssertCmd/*!*/ a = new AssertCmd(tok, expr);

         Contract.Assert(a != null);

+        if (Attributes != null)

+        {

+          // Inherit attributes of call.

+          var attrCopy = (QKeyValue)cce.NonNull(Attributes.Clone());

+          attrCopy = Substituter.Apply(s, attrCopy);

+          a.Attributes = attrCopy;

+        }

         a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr);

         newBlockBody.Add(a);

       }