Dafny: a partial first crack at a Dafny model-viewer provider, including captureState mark-ups in the Boogie code generated from Dafny

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 3e5ff0c3..3d1df65e 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -123,6 +123,13 @@ namespace Microsoft.Boogie
         }

       }

 

+      public IEnumerable<FuncTuple> AppsWithArgs(int argIdx0, Element elt0, int argIdx1, Element elt1) {

+        foreach (var r in elt0.References) {

+          if (r.Func == this && r.Args[argIdx0] == elt0 && r.Args[argIdx1] == elt1)

+            yield return r;

+        }

+      }

+

       public IEnumerable<FuncTuple> AppsWithResult(Element elt)

       {

         foreach (var r in elt.References) {