@@ -2023,13 +2023,6 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2023
2023
{{EOFv, EOFv}, {0 , UCharRangeMax}},
2024
2024
" an unsigned char value or EOF" )));
2025
2025
2026
- // The getc() family of functions that returns either a char or an EOF.
2027
- addToFunctionSummaryMap (
2028
- {" getc" , " fgetc" }, Signature (ArgTypes{FilePtrTy}, RetType{IntTy}),
2029
- Summary (NoEvalCall)
2030
- .Case ({ReturnValueCondition (WithinRange,
2031
- {{EOFv, EOFv}, {0 , UCharRangeMax}})},
2032
- ErrnoIrrelevant));
2033
2026
addToFunctionSummaryMap (
2034
2027
" getchar" , Signature (ArgTypes{}, RetType{IntTy}),
2035
2028
Summary (NoEvalCall)
@@ -2139,7 +2132,17 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2139
2132
std::move (GetenvSummary));
2140
2133
}
2141
2134
2142
- if (ModelPOSIX) {
2135
+ if (!ModelPOSIX) {
2136
+ // Without POSIX use of 'errno' is not specified (in these cases).
2137
+ // Add these functions without 'errno' checks.
2138
+ addToFunctionSummaryMap (
2139
+ {" getc" , " fgetc" }, Signature (ArgTypes{FilePtrTy}, RetType{IntTy}),
2140
+ Summary (NoEvalCall)
2141
+ .Case ({ReturnValueCondition (WithinRange,
2142
+ {{EOFv, EOFv}, {0 , UCharRangeMax}})},
2143
+ ErrnoIrrelevant)
2144
+ .ArgConstraint (NotNull (ArgNo (0 ))));
2145
+ } else {
2143
2146
const auto ReturnsZeroOrMinusOne =
2144
2147
ConstraintSet{ReturnValueCondition (WithinRange, Range (-1 , 0 ))};
2145
2148
const auto ReturnsZero =
@@ -2192,6 +2195,16 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2192
2195
.ArgConstraint (NotNull (ArgNo (1 )))
2193
2196
.ArgConstraint (NotNull (ArgNo (2 ))));
2194
2197
2198
+ // FILE *fdopen(int fd, const char *mode);
2199
+ addToFunctionSummaryMap (
2200
+ " fdopen" ,
2201
+ Signature (ArgTypes{IntTy, ConstCharPtrTy}, RetType{FilePtrTy}),
2202
+ Summary (NoEvalCall)
2203
+ .Case ({NotNull (Ret)}, ErrnoMustNotBeChecked, GenericSuccessMsg)
2204
+ .Case ({IsNull (Ret)}, ErrnoNEZeroIrrelevant, GenericFailureMsg)
2205
+ .ArgConstraint (ArgumentCondition (0 , WithinRange, Range (0 , IntMax)))
2206
+ .ArgConstraint (NotNull (ArgNo (1 ))));
2207
+
2195
2208
// int fclose(FILE *stream);
2196
2209
addToFunctionSummaryMap (
2197
2210
" fclose" , Signature (ArgTypes{FilePtrTy}, RetType{IntTy}),
@@ -2201,6 +2214,56 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2201
2214
ErrnoNEZeroIrrelevant, GenericFailureMsg)
2202
2215
.ArgConstraint (NotNull (ArgNo (0 ))));
2203
2216
2217
+ // int fgetc(FILE *stream);
2218
+ // 'getc' is the same as 'fgetc' but may be a macro
2219
+ addToFunctionSummaryMap (
2220
+ {" getc" , " fgetc" }, Signature (ArgTypes{FilePtrTy}, RetType{IntTy}),
2221
+ Summary (NoEvalCall)
2222
+ .Case ({ReturnValueCondition (WithinRange, {{0 , UCharRangeMax}})},
2223
+ ErrnoMustNotBeChecked, GenericSuccessMsg)
2224
+ .Case ({ReturnValueCondition (WithinRange, SingleValue (EOFv))},
2225
+ ErrnoNEZeroIrrelevant, GenericFailureMsg)
2226
+ .ArgConstraint (NotNull (ArgNo (0 ))));
2227
+
2228
+ // int fputc(int c, FILE *stream);
2229
+ // 'putc' is the same as 'fputc' but may be a macro
2230
+ addToFunctionSummaryMap (
2231
+ {" putc" , " fputc" },
2232
+ Signature (ArgTypes{IntTy, FilePtrTy}, RetType{IntTy}),
2233
+ Summary (NoEvalCall)
2234
+ .Case ({ReturnValueCondition (BO_EQ, ArgNo (0 ))},
2235
+ ErrnoMustNotBeChecked, GenericSuccessMsg)
2236
+ .Case ({ReturnValueCondition (WithinRange, SingleValue (EOFv))},
2237
+ ErrnoNEZeroIrrelevant, GenericFailureMsg)
2238
+ .ArgConstraint (NotNull (ArgNo (1 )))
2239
+ .ArgConstraint (
2240
+ ArgumentCondition (0 , WithinRange, {{0 , UCharRangeMax}})));
2241
+
2242
+ // char *fgets(char *restrict s, int n, FILE *restrict stream);
2243
+ addToFunctionSummaryMap (
2244
+ " fgets" ,
2245
+ Signature (ArgTypes{CharPtrRestrictTy, IntTy, FilePtrRestrictTy},
2246
+ RetType{CharPtrTy}),
2247
+ Summary (NoEvalCall)
2248
+ .Case ({ReturnValueCondition (BO_EQ, ArgNo (0 ))},
2249
+ ErrnoMustNotBeChecked, GenericSuccessMsg)
2250
+ .Case ({IsNull (Ret)}, ErrnoNEZeroIrrelevant, GenericFailureMsg)
2251
+ .ArgConstraint (NotNull (ArgNo (0 )))
2252
+ .ArgConstraint (ArgumentCondition (1 , WithinRange, Range (0 , IntMax)))
2253
+ .ArgConstraint (NotNull (ArgNo (2 ))));
2254
+
2255
+ // int fputs(const char *restrict s, FILE *restrict stream);
2256
+ addToFunctionSummaryMap (
2257
+ " fputs" ,
2258
+ Signature (ArgTypes{ConstCharPtrRestrictTy, FilePtrRestrictTy},
2259
+ RetType{IntTy}),
2260
+ Summary (NoEvalCall)
2261
+ .Case (ReturnsNonnegative, ErrnoMustNotBeChecked, GenericSuccessMsg)
2262
+ .Case ({ReturnValueCondition (WithinRange, SingleValue (EOFv))},
2263
+ ErrnoNEZeroIrrelevant, GenericFailureMsg)
2264
+ .ArgConstraint (NotNull (ArgNo (0 )))
2265
+ .ArgConstraint (NotNull (ArgNo (1 ))));
2266
+
2204
2267
// int fseek(FILE *stream, long offset, int whence);
2205
2268
// FIXME: It can be possible to get the 'SEEK_' values (like EOFv) and use
2206
2269
// these for condition of arg 2.
@@ -2800,15 +2863,6 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2800
2863
" pathconf" , Signature (ArgTypes{ConstCharPtrTy, IntTy}, RetType{LongTy}),
2801
2864
Summary (NoEvalCall).ArgConstraint (NotNull (ArgNo (0 ))));
2802
2865
2803
- // FILE *fdopen(int fd, const char *mode);
2804
- // FIXME: Improve for errno modeling.
2805
- addToFunctionSummaryMap (
2806
- " fdopen" ,
2807
- Signature (ArgTypes{IntTy, ConstCharPtrTy}, RetType{FilePtrTy}),
2808
- Summary (NoEvalCall)
2809
- .ArgConstraint (ArgumentCondition (0 , WithinRange, Range (0 , IntMax)))
2810
- .ArgConstraint (NotNull (ArgNo (1 ))));
2811
-
2812
2866
// void rewinddir(DIR *dir);
2813
2867
addToFunctionSummaryMap (
2814
2868
" rewinddir" , Signature (ArgTypes{DirPtrTy}, RetType{VoidTy}),
0 commit comments