================
@@ -916,6 +922,44 @@ void StreamChecker::evalFputx(const FnDescription *Desc,
const CallEvent &Call,
C.addTransition(StateFailed);
}
+void StreamChecker::evalUngetc(const FnDescription *Desc, const CallEvent
&Call,
+ CheckerContext &C) const {
+ ProgramStateRef State = C.getState();
+ SymbolRef StreamSym = getStreamArg(Desc, Call).getAsSymbol();
+ if (!StreamSym)
+ return;
+
+ const CallExpr *CE = dyn_cast_or_null<CallExpr>(Call.getOriginExpr());
+ if (!CE)
+ return;
+
+ const StreamState *OldSS = State->get<StreamMap>(StreamSym);
+ if (!OldSS)
+ return;
+
+ assertStreamStateOpened(OldSS);
+
+ // Generate a transition for the success state.
+ std::optional<NonLoc> PutVal = Call.getArgSVal(0).getAs<NonLoc>();
+ if (!PutVal)
+ return;
+ ProgramStateRef StateNotFailed =
+ State->BindExpr(CE, C.getLocationContext(), *PutVal);
+ StateNotFailed =
+ StateNotFailed->set<StreamMap>(StreamSym, StreamState::getOpened(Desc));
+ C.addTransition(StateNotFailed);
+
+ // Add transition for the failed state.
+ // Failure of 'ungetc' does not result in feof or ferror state.
+ // If the PutVal has value of EofVal the function should "fail", but this is
+ // the same transition as the success state.
+ // FIXME: Is it possible that StateFailed == StateNotFailed ?
----------------
NagyDonat wrote:
I strongly suspect that StateFailed == StateNotFailed (more precisely semantic
equivalence of the states, I don't know about the actual result of `operator==`
on `ProgramStateRef` values) is possible in the case when the first argument of
`ungetc` is a concrete `EOF` value.
I'd personally guess that this doesn't cause too much harm (at most there'll be
a redundantly duplicated edge that doesn't disturb the graph traversal), but if
you want to be on the safe side, you could investigate this with a testcase and
some exploded graph dumps.
https://github.com/llvm/llvm-project/pull/77331
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
