@@ -263,6 +263,9 @@ class StreamChecker : public Checker<check::PreCall, eval::Call,
263
263
{{{" fputs" }, 2 },
264
264
{std::bind (&StreamChecker::preReadWrite, _1, _2, _3, _4, false ),
265
265
std::bind (&StreamChecker::evalFputx, _1, _2, _3, _4, false ), 1 }},
266
+ {{{" fprintf" }},
267
+ {std::bind (&StreamChecker::preReadWrite, _1, _2, _3, _4, false ),
268
+ std::bind (&StreamChecker::evalFprintf, _1, _2, _3, _4), 0 }},
266
269
{{{" ungetc" }, 2 },
267
270
{std::bind (&StreamChecker::preReadWrite, _1, _2, _3, _4, false ),
268
271
std::bind (&StreamChecker::evalUngetc, _1, _2, _3, _4), 1 }},
@@ -339,6 +342,9 @@ class StreamChecker : public Checker<check::PreCall, eval::Call,
339
342
void evalFputx (const FnDescription *Desc, const CallEvent &Call,
340
343
CheckerContext &C, bool IsSingleChar) const ;
341
344
345
+ void evalFprintf (const FnDescription *Desc, const CallEvent &Call,
346
+ CheckerContext &C) const ;
347
+
342
348
void evalUngetc (const FnDescription *Desc, const CallEvent &Call,
343
349
CheckerContext &C) const ;
344
350
@@ -926,6 +932,49 @@ void StreamChecker::evalFputx(const FnDescription *Desc, const CallEvent &Call,
926
932
C.addTransition (StateFailed);
927
933
}
928
934
935
+ void StreamChecker::evalFprintf (const FnDescription *Desc,
936
+ const CallEvent &Call,
937
+ CheckerContext &C) const {
938
+ ProgramStateRef State = C.getState ();
939
+ if (Call.getNumArgs () < 2 )
940
+ return ;
941
+ SymbolRef StreamSym = getStreamArg (Desc, Call).getAsSymbol ();
942
+ if (!StreamSym)
943
+ return ;
944
+
945
+ const CallExpr *CE = dyn_cast_or_null<CallExpr>(Call.getOriginExpr ());
946
+ if (!CE)
947
+ return ;
948
+
949
+ const StreamState *OldSS = State->get <StreamMap>(StreamSym);
950
+ if (!OldSS)
951
+ return ;
952
+
953
+ assertStreamStateOpened (OldSS);
954
+
955
+ NonLoc RetVal = makeRetVal (C, CE).castAs <NonLoc>();
956
+ State = State->BindExpr (CE, C.getLocationContext (), RetVal);
957
+ SValBuilder &SVB = C.getSValBuilder ();
958
+ auto &ACtx = C.getASTContext ();
959
+ auto Cond = SVB.evalBinOp (State, BO_GE, RetVal, SVB.makeZeroVal (ACtx.IntTy ),
960
+ SVB.getConditionType ())
961
+ .getAs <DefinedOrUnknownSVal>();
962
+ if (!Cond)
963
+ return ;
964
+ ProgramStateRef StateNotFailed, StateFailed;
965
+ std::tie (StateNotFailed, StateFailed) = State->assume (*Cond);
966
+
967
+ StateNotFailed =
968
+ StateNotFailed->set <StreamMap>(StreamSym, StreamState::getOpened (Desc));
969
+ C.addTransition (StateNotFailed);
970
+
971
+ // Add transition for the failed state. The resulting value of the file
972
+ // position indicator for the stream is indeterminate.
973
+ StateFailed = StateFailed->set <StreamMap>(
974
+ StreamSym, StreamState::getOpened (Desc, ErrorFError, true ));
975
+ C.addTransition (StateFailed);
976
+ }
977
+
929
978
void StreamChecker::evalUngetc (const FnDescription *Desc, const CallEvent &Call,
930
979
CheckerContext &C) const {
931
980
ProgramStateRef State = C.getState ();
0 commit comments