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
|
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;
private final 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.
*
* <p>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;
}
}
|
