blob: 1ebd11b264f6f6347917251e49930e9b3c6fb544 (
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
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.Boogie.AbstractInterpretation
{
using System;
using System.Collections;
using System.Collections.Generic;
using Microsoft.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;
public List<AI.IVariable!>! FreeVariables
{
get
{
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)
{
if (expr is AI.IVariable)
{
if(!variables.Contains((AI.IVariable) expr))
{
this.variables.Add((AI.IVariable) expr);
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
{
assert false;
}
}
public override object VisitFunApp(AI.IFunApp! funapp)
{
foreach (AI.IExpr! arg in funapp.Arguments)
{
arg.DoVisit(this);
}
return true;
}
public override object VisitFunction(AI.IFunction! fun)
{
fun.Body.DoVisit(this);
this.variables.Remove(fun.Param);
return true;
}
}
}
|
