@@ -101,6 +101,21 @@ predicate functionArgumentMustBeNullTerminated(Function f, int i) {
101
101
f instanceof StrcatFunction and i = 0
102
102
}
103
103
104
+ /**
105
+ * Holds if `arg` is a string format argument to a formatting function call
106
+ * `ffc`.
107
+ */
108
+ predicate formatArgumentMustBeNullTerminated ( FormattingFunctionCall ffc , Expr arg ) {
109
+ // String argument to a formatting function (such as `printf`)
110
+ exists ( int n , FormatLiteral fl |
111
+ ffc .getConversionArgument ( n ) = arg and
112
+ fl = ffc .getFormat ( ) and
113
+ fl .getConversionType ( n ) instanceof PointerType and // `%s`, `%ws` etc
114
+ not fl .getConversionType ( n ) instanceof VoidPointerType and // exclude: `%p`
115
+ not fl .hasPrecision ( n ) // exclude: `%.*s`
116
+ )
117
+ }
118
+
104
119
/**
105
120
* Holds if `va` is a variable access where the contents must be null terminated.
106
121
*/
@@ -113,13 +128,7 @@ predicate variableMustBeNullTerminated(VariableAccess va) {
113
128
)
114
129
or
115
130
// String argument to a formatting function (such as `printf`)
116
- exists ( int n , FormatLiteral fl |
117
- fc .( FormattingFunctionCall ) .getConversionArgument ( n ) = va and
118
- fl = fc .( FormattingFunctionCall ) .getFormat ( ) and
119
- fl .getConversionType ( n ) instanceof PointerType and // `%s`, `%ws` etc
120
- not fl .getConversionType ( n ) instanceof VoidPointerType and // exclude: `%p`
121
- not fl .hasPrecision ( n ) // exclude: `%.*s`
122
- )
131
+ formatArgumentMustBeNullTerminated ( fc , va )
123
132
or
124
133
// Call to a wrapper function that requires null termination
125
134
// (not itself adding a null terminator)
0 commit comments