@@ -2220,6 +2220,9 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2220
2220
0 , WithinRange, {{EOFv, EOFv}, {0 , UCharRangeMax}}))
2221
2221
.ArgConstraint (NotNull (ArgNo (1 ))));
2222
2222
2223
+ std::optional<QualType> Off_tTy = lookupTy (" off_t" );
2224
+ std::optional<RangeInt> Off_tMax = getMaxValue (Off_tTy);
2225
+
2223
2226
// int fseek(FILE *stream, long offset, int whence);
2224
2227
// FIXME: It can be possible to get the 'SEEK_' values (like EOFv) and use
2225
2228
// these for condition of arg 2.
@@ -2232,6 +2235,16 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2232
2235
.ArgConstraint (NotNull (ArgNo (0 )))
2233
2236
.ArgConstraint (ArgumentCondition (2 , WithinRange, {{0 , 2 }})));
2234
2237
2238
+ // int fseeko(FILE *stream, off_t offset, int whence);
2239
+ addToFunctionSummaryMap (
2240
+ " fseeko" ,
2241
+ Signature (ArgTypes{FilePtrTy, Off_tTy, IntTy}, RetType{IntTy}),
2242
+ Summary (NoEvalCall)
2243
+ .Case (ReturnsZero, ErrnoMustNotBeChecked, GenericSuccessMsg)
2244
+ .Case (ReturnsMinusOne, ErrnoNEZeroIrrelevant, GenericFailureMsg)
2245
+ .ArgConstraint (NotNull (ArgNo (0 )))
2246
+ .ArgConstraint (ArgumentCondition (2 , WithinRange, {{0 , 2 }})));
2247
+
2235
2248
// int fgetpos(FILE *restrict stream, fpos_t *restrict pos);
2236
2249
// From 'The Open Group Base Specifications Issue 7, 2018 edition':
2237
2250
// "The fgetpos() function shall not change the setting of errno if
@@ -2279,6 +2292,15 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2279
2292
.Case (ReturnsMinusOne, ErrnoNEZeroIrrelevant, GenericFailureMsg)
2280
2293
.ArgConstraint (NotNull (ArgNo (0 ))));
2281
2294
2295
+ // off_t ftello(FILE *stream);
2296
+ addToFunctionSummaryMap (
2297
+ " ftello" , Signature (ArgTypes{FilePtrTy}, RetType{Off_tTy}),
2298
+ Summary (NoEvalCall)
2299
+ .Case ({ReturnValueCondition (WithinRange, Range (0 , Off_tMax))},
2300
+ ErrnoMustNotBeChecked, GenericSuccessMsg)
2301
+ .Case (ReturnsMinusOne, ErrnoNEZeroIrrelevant, GenericFailureMsg)
2302
+ .ArgConstraint (NotNull (ArgNo (0 ))));
2303
+
2282
2304
// int fileno(FILE *stream);
2283
2305
addToFunctionSummaryMap (
2284
2306
" fileno" , Signature (ArgTypes{FilePtrTy}, RetType{IntTy}),
@@ -2410,8 +2432,6 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2410
2432
.ArgConstraint (
2411
2433
ArgumentCondition (0 , WithinRange, Range (0 , IntMax))));
2412
2434
2413
- std::optional<QualType> Off_tTy = lookupTy (" off_t" );
2414
-
2415
2435
// int truncate(const char *path, off_t length);
2416
2436
addToFunctionSummaryMap (
2417
2437
" truncate" ,
@@ -2854,19 +2874,6 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
2854
2874
" rand_r" , Signature (ArgTypes{UnsignedIntPtrTy}, RetType{IntTy}),
2855
2875
Summary (NoEvalCall).ArgConstraint (NotNull (ArgNo (0 ))));
2856
2876
2857
- // int fseeko(FILE *stream, off_t offset, int whence);
2858
- addToFunctionSummaryMap (
2859
- " fseeko" ,
2860
- Signature (ArgTypes{FilePtrTy, Off_tTy, IntTy}, RetType{IntTy}),
2861
- Summary (NoEvalCall)
2862
- .Case (ReturnsZeroOrMinusOne, ErrnoIrrelevant)
2863
- .ArgConstraint (NotNull (ArgNo (0 ))));
2864
-
2865
- // off_t ftello(FILE *stream);
2866
- addToFunctionSummaryMap (
2867
- " ftello" , Signature (ArgTypes{FilePtrTy}, RetType{Off_tTy}),
2868
- Summary (NoEvalCall).ArgConstraint (NotNull (ArgNo (0 ))));
2869
-
2870
2877
// void *mmap(void *addr, size_t length, int prot, int flags, int fd,
2871
2878
// off_t offset);
2872
2879
// FIXME: Improve for errno modeling.
0 commit comments