@@ -266,6 +266,8 @@ class StreamChecker : public Checker<check::PreCall, eval::Call,
266
266
{&StreamChecker::preFseek, &StreamChecker::evalFseek, 0 }},
267
267
{{{" ftell" }, 1 },
268
268
{&StreamChecker::preDefault, &StreamChecker::evalFtell, 0 }},
269
+ {{{" fflush" }, 1 },
270
+ {&StreamChecker::preFflush, &StreamChecker::evalFflush, 0 }},
269
271
{{{" rewind" }, 1 },
270
272
{&StreamChecker::preDefault, &StreamChecker::evalRewind, 0 }},
271
273
{{{" fgetpos" }, 2 },
@@ -360,6 +362,12 @@ class StreamChecker : public Checker<check::PreCall, eval::Call,
360
362
CheckerContext &C,
361
363
const StreamErrorState &ErrorKind) const ;
362
364
365
+ void preFflush (const FnDescription *Desc, const CallEvent &Call,
366
+ CheckerContext &C) const ;
367
+
368
+ void evalFflush (const FnDescription *Desc, const CallEvent &Call,
369
+ CheckerContext &C) const ;
370
+
363
371
// / Check that the stream (in StreamVal) is not NULL.
364
372
// / If it can only be NULL a fatal error is emitted and nullptr returned.
365
373
// / Otherwise the return value is a new state where the stream is constrained
@@ -1191,6 +1199,84 @@ void StreamChecker::evalSetFeofFerror(const FnDescription *Desc,
1191
1199
C.addTransition (State);
1192
1200
}
1193
1201
1202
+ void StreamChecker::preFflush (const FnDescription *Desc, const CallEvent &Call,
1203
+ CheckerContext &C) const {
1204
+ ProgramStateRef State = C.getState ();
1205
+ SVal StreamVal = getStreamArg (Desc, Call);
1206
+ std::optional<DefinedSVal> Stream = StreamVal.getAs <DefinedSVal>();
1207
+ if (!Stream)
1208
+ return ;
1209
+
1210
+ ProgramStateRef StateNotNull, StateNull;
1211
+ std::tie (StateNotNull, StateNull) =
1212
+ C.getConstraintManager ().assumeDual (State, *Stream);
1213
+ if (StateNotNull && !StateNull)
1214
+ ensureStreamOpened (StreamVal, C, StateNotNull);
1215
+ }
1216
+
1217
+ void StreamChecker::evalFflush (const FnDescription *Desc, const CallEvent &Call,
1218
+ CheckerContext &C) const {
1219
+ ProgramStateRef State = C.getState ();
1220
+ SVal StreamVal = getStreamArg (Desc, Call);
1221
+ std::optional<DefinedSVal> Stream = StreamVal.getAs <DefinedSVal>();
1222
+ if (!Stream)
1223
+ return ;
1224
+
1225
+ // Skip if the stream can be both NULL and non-NULL.
1226
+ ProgramStateRef StateNotNull, StateNull;
1227
+ std::tie (StateNotNull, StateNull) =
1228
+ C.getConstraintManager ().assumeDual (State, *Stream);
1229
+ if (StateNotNull && StateNull)
1230
+ return ;
1231
+ if (StateNotNull && !StateNull)
1232
+ State = StateNotNull;
1233
+ else
1234
+ State = StateNull;
1235
+
1236
+ const CallExpr *CE = dyn_cast_or_null<CallExpr>(Call.getOriginExpr ());
1237
+ if (!CE)
1238
+ return ;
1239
+
1240
+ // `fflush` returns EOF on failure, otherwise returns 0.
1241
+ ProgramStateRef StateFailed = bindInt (*EofVal, State, C, CE);
1242
+ ProgramStateRef StateNotFailed = bindInt (0 , State, C, CE);
1243
+
1244
+ // Clear error states if `fflush` returns 0, but retain their EOF flags.
1245
+ auto ClearErrorInNotFailed = [&StateNotFailed, Desc](SymbolRef Sym,
1246
+ const StreamState *SS) {
1247
+ if (SS->ErrorState & ErrorFError) {
1248
+ StreamErrorState NewES =
1249
+ (SS->ErrorState & ErrorFEof) ? ErrorFEof : ErrorNone;
1250
+ StreamState NewSS = StreamState::getOpened (Desc, NewES, false );
1251
+ StateNotFailed = StateNotFailed->set <StreamMap>(Sym, NewSS);
1252
+ }
1253
+ };
1254
+
1255
+ if (StateNotNull && !StateNull) {
1256
+ // Skip if the input stream's state is unknown, open-failed or closed.
1257
+ if (SymbolRef StreamSym = StreamVal.getAsSymbol ()) {
1258
+ const StreamState *SS = State->get <StreamMap>(StreamSym);
1259
+ if (SS) {
1260
+ assert (SS->isOpened () && " Stream is expected to be opened" );
1261
+ ClearErrorInNotFailed (StreamSym, SS);
1262
+ } else
1263
+ return ;
1264
+ }
1265
+ } else {
1266
+ // Clear error states for all streams.
1267
+ const StreamMapTy &Map = StateNotFailed->get <StreamMap>();
1268
+ for (const auto &I : Map) {
1269
+ SymbolRef Sym = I.first ;
1270
+ const StreamState &SS = I.second ;
1271
+ if (SS.isOpened ())
1272
+ ClearErrorInNotFailed (Sym, &SS);
1273
+ }
1274
+ }
1275
+
1276
+ C.addTransition (StateNotFailed);
1277
+ C.addTransition (StateFailed);
1278
+ }
1279
+
1194
1280
ProgramStateRef
1195
1281
StreamChecker::ensureStreamNonNull (SVal StreamVal, const Expr *StreamE,
1196
1282
CheckerContext &C,
0 commit comments