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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
package org.checkerframework.dataflow.analysis;
import java.util.Map;
import javax.lang.model.type.TypeMirror;
/**
* Implementation of a {@link TransferResult} with just one non-exceptional
* store. The result of {@code getThenStore} and {@code getElseStore} is equal
* to the only underlying store.
*
* @author Stefan Heule
*
* @param <S>
* The {@link Store} used to keep track of intermediate results.
*/
public class RegularTransferResult<A extends AbstractValue<A>, S extends Store<S>>
extends TransferResult<A, S> {
/** The regular result store. */
protected S store;
final private boolean storeChanged;
/**
* Create a {@code TransferResult} with {@code resultStore} as the resulting
* store. If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} is a boolean node, then
* {@code resultStore} is used for both the 'then' and 'else' edge.
*
* <p>
*
* <em>Exceptions</em>: If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} throws an
* exception, then it is assumed that no special handling is necessary and
* the store before the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any
* exceptional edge.
*
* <p>
*
* <em>Aliasing</em>: {@code resultStore} is not allowed to be used anywhere
* outside of this class (including use through aliases). Complete control
* over the object is transfered to this class.
*/
public RegularTransferResult(A value, S resultStore, boolean storeChanged) {
super(value);
this.store = resultStore;
this.storeChanged = storeChanged;
}
public RegularTransferResult(A value, S resultStore) {
this(value, resultStore, false);
}
/**
* Create a {@code TransferResult} with {@code resultStore} as the resulting
* store. If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} is a boolean node, then
* {@code resultStore} is used for both the 'then' and 'else' edge.
*
* For the meaning of storeChanged, see
* {@link org.checkerframework.dataflow.analysis.TransferResult#storeChanged}.
*
* <p>
*
* <em>Exceptions</em>: If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} throws an
* exception, then the corresponding store in {@code exceptionalStores} is
* used. If no exception is found in {@code exceptionalStores}, then it is
* assumed that no special handling is necessary and the store before the
* corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge.
*
* <p>
*
* <em>Aliasing</em>: {@code resultStore} and any store in
* {@code exceptionalStores} are not allowed to be used anywhere outside of
* this class (including use through aliases). Complete control over the
* objects is transfered to this class.
*/
public RegularTransferResult(A value, S resultStore,
Map<TypeMirror, S> exceptionalStores, boolean storeChanged) {
super(value);
this.store = resultStore;
this.storeChanged = storeChanged;
this.exceptionalStores = exceptionalStores;
}
public RegularTransferResult(A value, S resultStore,
Map<TypeMirror, S> exceptionalStores) {
this(value, resultStore, exceptionalStores, false);
}
@Override
public S getRegularStore() {
return store;
}
@Override
public S getThenStore() {
return store;
}
@Override
public S getElseStore() {
// copy the store such that it is the same as the result of getThenStore
// (that is, identical according to equals), but two different objects.
return store.copy();
}
@Override
public boolean containsTwoStores() {
return false;
}
@Override
public String toString() {
StringBuilder result = new StringBuilder();
result.append("RegularTransferResult(");
result.append(System.getProperty("line.separator"));
result.append("resultValue = " + resultValue);
result.append(System.getProperty("line.separator"));
result.append("store = " + store);
result.append(System.getProperty("line.separator"));
result.append(")");
return result.toString();
}
/**
* @see org.checkerframework.dataflow.analysis.TransferResult#storeChanged()
*/
@Override
public boolean storeChanged() {
return storeChanged;
}
}
|
