blob: 5bb5916d0c895190201e669b9b1bcd5cb29db673 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.Boogie.AbstractInterpretation {
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using AI = Microsoft.AbstractInterpretationFramework;
using Boogie = Microsoft.Boogie;
/// <summary>
/// A visitor of an abstract interpretation expression that collects the free variables
/// </summary>
class FreeVariablesVisitor : AI.ExprVisitor {
[Peer]
List<AI.IVariable> variables;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(variables));
Contract.Invariant(cce.NonNullElements(varNames));
}
public List<AI.IVariable> FreeVariables {
get {
Contract.Ensures(cce.NonNullElements(Contract.Result<List<AI.IVariable>>()));
return this.variables;
}
}
List<string> varNames; // used to check the consinstency!
public FreeVariablesVisitor() {
this.variables = new List<AI.IVariable>();
this.varNames = new List<string>();
}
override public object Default(AI.IExpr expr) {
Contract.Requires(expr != null);
if (expr is AI.IVariable) {
if (!variables.Contains((AI.IVariable)expr)) {
this.variables.Add((AI.IVariable)expr);
Contract.Assert(!this.varNames.Contains(expr.ToString())); // If we get there, we have an error: two variables with the same name but different identity
this.varNames.Add(expr.ToString());
}
return null;
} else if (expr is AI.IFunApp)
return VisitFunApp((AI.IFunApp)expr);
else if (expr is AI.IFunction)
return VisitFunction((AI.IFunction)expr);
else if (expr is AI.IUnknown)
return null;
else {
Contract.Assert(false);
throw new cce.UnreachableException();
}
}
public override object VisitFunApp(AI.IFunApp funapp) {
Contract.Requires(funapp != null);
foreach (AI.IExpr arg in funapp.Arguments) {
Contract.Assert(arg != null);
arg.DoVisit(this);
}
return true;
}
public override object VisitFunction(AI.IFunction fun) {
Contract.Requires(fun != null);
fun.Body.DoVisit(this);
this.variables.Remove(fun.Param);
return true;
}
}
}
|
