@@ -252,7 +252,10 @@ class StreamChecker : public Checker<check::PreCall, eval::Call,
252
252
std::bind (&StreamChecker::evalFreadFwrite, _1, _2, _3, _4, false ), 3 }},
253
253
{{{" fgetc" }, 1 },
254
254
{std::bind (&StreamChecker::preReadWrite, _1, _2, _3, _4, true ),
255
- std::bind (&StreamChecker::evalFgetc, _1, _2, _3, _4), 0 }},
255
+ std::bind (&StreamChecker::evalFgetx, _1, _2, _3, _4, true ), 0 }},
256
+ {{{" fgets" }, 3 },
257
+ {std::bind (&StreamChecker::preReadWrite, _1, _2, _3, _4, true ),
258
+ std::bind (&StreamChecker::evalFgetx, _1, _2, _3, _4, false ), 2 }},
256
259
{{{" fputc" }, 2 },
257
260
{std::bind (&StreamChecker::preReadWrite, _1, _2, _3, _4, false ),
258
261
std::bind (&StreamChecker::evalFputx, _1, _2, _3, _4, true ), 1 }},
@@ -320,8 +323,8 @@ class StreamChecker : public Checker<check::PreCall, eval::Call,
320
323
void evalFreadFwrite (const FnDescription *Desc, const CallEvent &Call,
321
324
CheckerContext &C, bool IsFread) const ;
322
325
323
- void evalFgetc (const FnDescription *Desc, const CallEvent &Call,
324
- CheckerContext &C) const ;
326
+ void evalFgetx (const FnDescription *Desc, const CallEvent &Call,
327
+ CheckerContext &C, bool SingleChar ) const ;
325
328
326
329
void evalFputx (const FnDescription *Desc, const CallEvent &Call,
327
330
CheckerContext &C, bool IsSingleChar) const ;
@@ -760,8 +763,8 @@ void StreamChecker::evalFreadFwrite(const FnDescription *Desc,
760
763
C.addTransition (StateFailed);
761
764
}
762
765
763
- void StreamChecker::evalFgetc (const FnDescription *Desc, const CallEvent &Call,
764
- CheckerContext &C) const {
766
+ void StreamChecker::evalFgetx (const FnDescription *Desc, const CallEvent &Call,
767
+ CheckerContext &C, bool SingleChar ) const {
765
768
ProgramStateRef State = C.getState ();
766
769
SymbolRef StreamSym = getStreamArg (Desc, Call).getAsSymbol ();
767
770
if (!StreamSym)
@@ -778,42 +781,61 @@ void StreamChecker::evalFgetc(const FnDescription *Desc, const CallEvent &Call,
778
781
assertStreamStateOpened (OldSS);
779
782
780
783
// `fgetc` returns the read character on success, otherwise returns EOF.
784
+ // `fgets` returns the read buffer address on success, otherwise returns NULL.
781
785
782
- // Generate a transition for the success state of `fgetc`.
783
- // If we know the state to be FEOF at fgetc, do not add a success state.
784
786
if (OldSS->ErrorState != ErrorFEof) {
785
- NonLoc RetVal = makeRetVal (C, CE).castAs <NonLoc>();
786
- ProgramStateRef StateNotFailed =
787
- State->BindExpr (CE, C.getLocationContext (), RetVal);
788
- SValBuilder &SVB = C.getSValBuilder ();
789
- ASTContext &ASTC = C.getASTContext ();
790
- // The returned 'unsigned char' of `fgetc` is converted to 'int',
791
- // so we need to check if it is in range [0, 255].
792
- auto CondLow =
793
- SVB.evalBinOp (State, BO_GE, RetVal, SVB.makeZeroVal (ASTC.IntTy ),
794
- SVB.getConditionType ())
795
- .getAs <DefinedOrUnknownSVal>();
796
- auto CondHigh =
797
- SVB.evalBinOp (State, BO_LE, RetVal,
798
- SVB.makeIntVal (SVB.getBasicValueFactory ()
799
- .getMaxValue (ASTC.UnsignedCharTy )
800
- .getLimitedValue (),
801
- ASTC.IntTy ),
802
- SVB.getConditionType ())
803
- .getAs <DefinedOrUnknownSVal>();
804
- if (!CondLow || !CondHigh)
805
- return ;
806
- StateNotFailed = StateNotFailed->assume (*CondLow, true );
807
- if (!StateNotFailed)
808
- return ;
809
- StateNotFailed = StateNotFailed->assume (*CondHigh, true );
810
- if (!StateNotFailed)
811
- return ;
812
- C.addTransition (StateNotFailed);
787
+ if (SingleChar) {
788
+ // Generate a transition for the success state of `fgetc`.
789
+ NonLoc RetVal = makeRetVal (C, CE).castAs <NonLoc>();
790
+ ProgramStateRef StateNotFailed =
791
+ State->BindExpr (CE, C.getLocationContext (), RetVal);
792
+ SValBuilder &SVB = C.getSValBuilder ();
793
+ ASTContext &ASTC = C.getASTContext ();
794
+ // The returned 'unsigned char' of `fgetc` is converted to 'int',
795
+ // so we need to check if it is in range [0, 255].
796
+ auto CondLow =
797
+ SVB.evalBinOp (State, BO_GE, RetVal, SVB.makeZeroVal (ASTC.IntTy ),
798
+ SVB.getConditionType ())
799
+ .getAs <DefinedOrUnknownSVal>();
800
+ auto CondHigh =
801
+ SVB.evalBinOp (State, BO_LE, RetVal,
802
+ SVB.makeIntVal (SVB.getBasicValueFactory ()
803
+ .getMaxValue (ASTC.UnsignedCharTy )
804
+ .getLimitedValue (),
805
+ ASTC.IntTy ),
806
+ SVB.getConditionType ())
807
+ .getAs <DefinedOrUnknownSVal>();
808
+ if (!CondLow || !CondHigh)
809
+ return ;
810
+ StateNotFailed = StateNotFailed->assume (*CondLow, true );
811
+ if (!StateNotFailed)
812
+ return ;
813
+ StateNotFailed = StateNotFailed->assume (*CondHigh, true );
814
+ if (!StateNotFailed)
815
+ return ;
816
+ C.addTransition (StateNotFailed);
817
+ } else {
818
+ // Generate a transition for the success state of `fgets`.
819
+ std::optional<DefinedSVal> GetBuf =
820
+ Call.getArgSVal (0 ).getAs <DefinedSVal>();
821
+ if (!GetBuf)
822
+ return ;
823
+ ProgramStateRef StateNotFailed =
824
+ State->BindExpr (CE, C.getLocationContext (), *GetBuf);
825
+ StateNotFailed = StateNotFailed->set <StreamMap>(
826
+ StreamSym, StreamState::getOpened (Desc));
827
+ C.addTransition (StateNotFailed);
828
+ }
813
829
}
814
830
815
831
// Add transition for the failed state.
816
- ProgramStateRef StateFailed = bindInt (*EofVal, State, C, CE);
832
+ ProgramStateRef StateFailed;
833
+ if (SingleChar)
834
+ StateFailed = bindInt (*EofVal, State, C, CE);
835
+ else
836
+ StateFailed =
837
+ State->BindExpr (CE, C.getLocationContext (),
838
+ C.getSValBuilder ().makeNullWithType (CE->getType ()));
817
839
818
840
// If a (non-EOF) error occurs, the resulting value of the file position
819
841
// indicator for the stream is indeterminate.
0 commit comments