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
|
using System;
using System.Numerics;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
namespace Microsoft.Boogie.AbstractInterpretation
{
class TrivialDomain : NativeLattice
{
class E : NativeLattice.Element
{
public readonly bool IsTop;
public E(bool isTop) {
IsTop = isTop;
}
public override Expr ToExpr() {
return Expr.Literal(IsTop);
}
}
private E top = new E(true);
private E bottom = new E(false);
public override Element Top { get { return top; } }
public override Element Bottom { get { return bottom; } }
public override bool IsTop(Element element) {
var e = (E)element;
return e.IsTop;
}
public override bool IsBottom(Element element) {
var e = (E)element;
return !e.IsTop;
}
public override bool Below(Element a, Element b) {
return IsBottom(a) || IsTop(b);
}
public override Element Meet(Element a, Element b) {
if (IsBottom(b)) {
return b;
} else {
return a;
}
}
public override Element Join(Element a, Element b) {
if (IsTop(b)) {
return b;
} else {
return a;
}
}
public override Element Widen(Element a, Element b) {
return Join(a, b); // it's a finite domain, after all
}
public override Element Constrain(Element element, Expr expr) {
var e = (E)element;
var lit = expr as LiteralExpr;
if (lit != null && lit.isBool && !(bool)lit.Val) {
return bottom;
} else {
return e;
}
}
public override Element Update(Element element, AssignCmd cmd) {
return element;
}
public override Element Eliminate(Element element, Variable v) {
return element;
}
}
}
|
