1
+ /**
2
+ * Provides classes for identifying and reasoning about Microsoft source code
3
+ * annotation language (SAL) macros.
4
+ */
5
+
1
6
import cpp
2
7
8
+ /**
9
+ * A SAL macro defined in `sal.h` or a similar header file.
10
+ */
3
11
class SALMacro extends Macro {
4
12
SALMacro ( ) {
5
13
exists ( string filename | filename = this .getFile ( ) .getBaseName ( ) |
@@ -20,27 +28,34 @@ class SALMacro extends Macro {
20
28
}
21
29
22
30
pragma [ noinline]
23
- predicate isTopLevelMacroAccess ( MacroAccess ma ) { not exists ( ma .getParentInvocation ( ) ) }
31
+ private predicate isTopLevelMacroAccess ( MacroAccess ma ) { not exists ( ma .getParentInvocation ( ) ) }
24
32
33
+ /**
34
+ * An invocation of a SAL macro (excluding invocations inside other macros).
35
+ */
25
36
class SALAnnotation extends MacroInvocation {
26
37
SALAnnotation ( ) {
27
38
this .getMacro ( ) instanceof SALMacro and
28
39
isTopLevelMacroAccess ( this )
29
40
}
30
41
31
- /** Returns the `Declaration` annotated by `this`. */
42
+ /** Gets the `Declaration` annotated by `this`. */
32
43
Declaration getDeclaration ( ) {
33
44
annotatesAt ( this , result .getADeclarationEntry ( ) , _, _) and
34
45
not result instanceof Type // exclude typedefs
35
46
}
36
47
37
- /** Returns the `DeclarationEntry` annotated by `this`. */
48
+ /** Gets the `DeclarationEntry` annotated by `this`. */
38
49
DeclarationEntry getDeclarationEntry ( ) {
39
50
annotatesAt ( this , result , _, _) and
40
51
not result instanceof TypeDeclarationEntry // exclude typedefs
41
52
}
42
53
}
43
54
55
+ /**
56
+ * A SAL macro indicating that the return value of a function should always be
57
+ * checked.
58
+ */
44
59
class SALCheckReturn extends SALAnnotation {
45
60
SALCheckReturn ( ) {
46
61
exists ( SALMacro m | m = this .getMacro ( ) |
@@ -50,6 +65,10 @@ class SALCheckReturn extends SALAnnotation {
50
65
}
51
66
}
52
67
68
+ /**
69
+ * A SAL macro indicating that a pointer variable or return value should not be
70
+ * `NULL`.
71
+ */
53
72
class SALNotNull extends SALAnnotation {
54
73
SALNotNull ( ) {
55
74
exists ( SALMacro m | m = this .getMacro ( ) |
@@ -69,6 +88,9 @@ class SALNotNull extends SALAnnotation {
69
88
}
70
89
}
71
90
91
+ /**
92
+ * A SAL macro indicating that a value may be `NULL`.
93
+ */
72
94
class SALMaybeNull extends SALAnnotation {
73
95
SALMaybeNull ( ) {
74
96
exists ( SALMacro m | m = this .getMacro ( ) |
@@ -79,13 +101,29 @@ class SALMaybeNull extends SALAnnotation {
79
101
}
80
102
}
81
103
104
+ /**
105
+ * A parameter annotated by one or more SAL annotations.
106
+ */
107
+ class SALParameter extends Parameter {
108
+ /** One of this parameter's annotations. */
109
+ SALAnnotation a ;
110
+
111
+ SALParameter ( ) { annotatesAt ( a , this .getADeclarationEntry ( ) , _, _) }
112
+
113
+ predicate isIn ( ) { a .getMacroName ( ) .toLowerCase ( ) .matches ( "%\\_in%" ) }
114
+
115
+ predicate isOut ( ) { a .getMacroName ( ) .toLowerCase ( ) .matches ( "%\\_out%" ) }
116
+
117
+ predicate isInOut ( ) { a .getMacroName ( ) .toLowerCase ( ) .matches ( "%\\_inout%" ) }
118
+ }
119
+
82
120
///////////////////////////////////////////////////////////////////////////////
83
121
// Implementation details
84
122
/**
85
123
* Holds if `a` annotates the declaration entry `d` and
86
124
* its start position is the `idx`th position in `file` that holds a SAL element.
87
125
*/
88
- predicate annotatesAt ( SALAnnotation a , DeclarationEntry d , File file , int idx ) {
126
+ private predicate annotatesAt ( SALAnnotation a , DeclarationEntry d , File file , int idx ) {
89
127
annotatesAtPosition ( a .( SALElement ) .getStartPosition ( ) , d , file , idx )
90
128
}
91
129
@@ -109,22 +147,6 @@ private predicate annotatesAtPosition(SALPosition pos, DeclarationEntry d, File
109
147
)
110
148
}
111
149
112
- /**
113
- * A parameter annotated by one or more SAL annotations.
114
- */
115
- class SALParameter extends Parameter {
116
- /** One of this parameter's annotations. */
117
- SALAnnotation a ;
118
-
119
- SALParameter ( ) { annotatesAt ( a , this .getADeclarationEntry ( ) , _, _) }
120
-
121
- predicate isIn ( ) { a .getMacroName ( ) .toLowerCase ( ) .matches ( "%\\_in%" ) }
122
-
123
- predicate isOut ( ) { a .getMacroName ( ) .toLowerCase ( ) .matches ( "%\\_out%" ) }
124
-
125
- predicate isInOut ( ) { a .getMacroName ( ) .toLowerCase ( ) .matches ( "%\\_inout%" ) }
126
- }
127
-
128
150
/**
129
151
* A SAL element, that is, a SAL annotation or a declaration entry
130
152
* that may have SAL annotations.
0 commit comments