1
1
/**
2
- * A module for considering whether a result occurs in all instances (e.g. copies) of the code at a
3
- * given location.
2
+ * A module for considering whether a result occurs in all copies of the code at a given location.
4
3
*
5
- * Multiple instances of an element at the same location can occur for two main reasons:
4
+ * Multiple copies of an element at the same location can occur for two main reasons:
6
5
* 1. Instantiations of a template
7
6
* 2. Re-compilation of a file under a different context
8
7
* This module helps ensure that a particular condition holds for all copies of a particular logical
@@ -37,17 +36,21 @@ predicate isNotWithinMacroExpansion(Element e) {
37
36
)
38
37
}
39
38
40
- /** A candidate set of elements. */
39
+ /**
40
+ * A type representing a set of Element's in the program that satisfy some condition.
41
+ *
42
+ * `HoldsForAllCopies<T>::LogicalResultElement` will represent an element in this set
43
+ * iff all copies of that element satisfy the condition.
44
+ */
41
45
signature class CandidateElementSig extends Element ;
42
46
43
47
/** The super set of relevant elements. */
44
48
signature class ElementSetSig extends Element ;
45
49
46
50
/**
47
- * A module for considering whether a result occurs in all instances (e.g. copies) of the code at a
48
- * given location.
51
+ * A module for considering whether a result occurs in all copies of the code at a given location.
49
52
*/
50
- module HoldsForAllInstances < CandidateElementSig CandidateElement, ElementSetSig ElementSet> {
53
+ module HoldsForAllCopies < CandidateElementSig CandidateElement, ElementSetSig ElementSet> {
51
54
private predicate hasLocation (
52
55
ElementSet s , string filepath , int startline , int startcolumn , int endline , int endcolumn
53
56
) {
@@ -93,8 +96,8 @@ module HoldsForAllInstances<CandidateElementSig CandidateElement, ElementSetSig
93
96
}
94
97
95
98
/**
96
- * A logical result element, representing all instances of a element that occur at the same
97
- * location.
99
+ * A logical result element representing all copies of an element that occur at the same
100
+ * location, iff they all belong to the `CandidateElement` set .
98
101
*/
99
102
class LogicalResultElement extends TLogicalResultElement {
100
103
predicate hasLocationInfo (
@@ -103,7 +106,7 @@ module HoldsForAllInstances<CandidateElementSig CandidateElement, ElementSetSig
103
106
this = TLogicalResultElement ( filepath , startline , startcolumn , endline , endcolumn )
104
107
}
105
108
106
- /** Gets an instance of this logical result element. */
109
+ /** Gets a copy instance of this logical result element. */
107
110
CandidateElement getAnElementInstance ( ) {
108
111
exists ( string filepath , int startline , int startcolumn , int endline , int endcolumn |
109
112
this = TLogicalResultElement ( filepath , startline , startcolumn , endline , endcolumn ) and
0 commit comments