diff options
| author |  rustanleino <unknown> | 2010-11-01 21:56:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-01 21:56:14 +0000 |
| commit | 31f5a7c20e25225e4b9dca95e60e955402f64df6 (patch) | |
| tree | a8b2a54790d1e1900ed0a7ea8d00bd6faa7ce31f /Source/Model | |
| parent | 1219dc1f931e17918d3a1bfe580149b21493a0c4 (diff) | |
Dafny: a partial first crack at a Dafny model-viewer provider, including captureState mark-ups in the Boogie code generated from Dafny
Diffstat (limited to 'Source/Model')
| -rw-r--r-- | Source/Model/Model.cs | 7 |
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) {
|