@@ -2236,7 +2236,7 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2236
2236
.Case ({ReturnValueCondition (WithinRange, {{0 , UCharRangeMax}})},
2237
2237
ErrnoMustNotBeChecked, GenericSuccessMsg)
2238
2238
.Case ({ReturnValueCondition (WithinRange, SingleValue (EOFv))},
2239
- ErrnoNEZeroIrrelevant , GenericFailureMsg)
2239
+ ErrnoIrrelevant , GenericFailureMsg)
2240
2240
.ArgConstraint (NotNull (ArgNo (0 ))));
2241
2241
2242
2242
// int fputc(int c, FILE *stream);
@@ -2245,13 +2245,15 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2245
2245
{" putc" , " fputc" },
2246
2246
Signature (ArgTypes{IntTy, FilePtrTy}, RetType{IntTy}),
2247
2247
Summary (NoEvalCall)
2248
- .Case ({ReturnValueCondition (BO_EQ, ArgNo (0 ))},
2248
+ .Case ({ArgumentCondition (0 , WithinRange, Range (0 , UCharRangeMax)),
2249
+ ReturnValueCondition (BO_EQ, ArgNo (0 ))},
2250
+ ErrnoMustNotBeChecked, GenericSuccessMsg)
2251
+ .Case ({ArgumentCondition (0 , OutOfRange, Range (0 , UCharRangeMax)),
2252
+ ReturnValueCondition (WithinRange, Range (0 , UCharRangeMax))},
2249
2253
ErrnoMustNotBeChecked, GenericSuccessMsg)
2250
2254
.Case ({ReturnValueCondition (WithinRange, SingleValue (EOFv))},
2251
2255
ErrnoNEZeroIrrelevant, GenericFailureMsg)
2252
- .ArgConstraint (NotNull (ArgNo (1 )))
2253
- .ArgConstraint (
2254
- ArgumentCondition (0 , WithinRange, {{0 , UCharRangeMax}})));
2256
+ .ArgConstraint (NotNull (ArgNo (1 ))));
2255
2257
2256
2258
// char *fgets(char *restrict s, int n, FILE *restrict stream);
2257
2259
addToFunctionSummaryMap (
@@ -2261,9 +2263,11 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2261
2263
Summary (NoEvalCall)
2262
2264
.Case ({ReturnValueCondition (BO_EQ, ArgNo (0 ))},
2263
2265
ErrnoMustNotBeChecked, GenericSuccessMsg)
2264
- .Case ({IsNull (Ret)}, ErrnoNEZeroIrrelevant , GenericFailureMsg)
2266
+ .Case ({IsNull (Ret)}, ErrnoIrrelevant , GenericFailureMsg)
2265
2267
.ArgConstraint (NotNull (ArgNo (0 )))
2266
2268
.ArgConstraint (ArgumentCondition (1 , WithinRange, Range (0 , IntMax)))
2269
+ .ArgConstraint (
2270
+ BufferSize (/* Buffer=*/ ArgNo (0 ), /* BufSize=*/ ArgNo (1 )))
2267
2271
.ArgConstraint (NotNull (ArgNo (2 ))));
2268
2272
2269
2273
// int fputs(const char *restrict s, FILE *restrict stream);
0 commit comments