Alejandro =?utf-8?q?Álvarez_Ayllón?Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/83...@github.com>
================
@@ -1183,6 +1315,20 @@ void StreamChecker::evalGetdelim(const FnDescription
*Desc,
State->BindExpr(E.CE, C.getLocationContext(), RetVal);
StateNotFailed =
E.assumeBinOpNN(StateNotFailed, BO_GE, RetVal, E.getZeroVal(Call));
+ // The buffer size `*n` must be enough to hold the whole line, and
+ // greater than the return value, since it has to account for '\0'.
+ auto SizePtrSval = Call.getArgSVal(1);
+ auto NVal = getPointeeDefVal(SizePtrSval, State);
+ if (NVal) {
+ StateNotFailed = StateNotFailed->assume(
+ E.SVB
+ .evalBinOp(StateNotFailed, BinaryOperator::Opcode::BO_GT, *NVal,
+ RetVal, E.SVB.getConditionType())
+ .castAs<DefinedOrUnknownSVal>(),
+ true);
----------------
steakhal wrote:
```suggestion
StateNotFailed = StateNotFailed->assume(
E.SVB
.evalBinOp(StateNotFailed, BO_GT, *NVal, RetVal,
E.SVB.getConditionType())
.castAs<DefinedOrUnknownSVal>(),
true);
```
I'm worried a bit that we already constrained retVal: `0 <= retVal`, with the
previous assumption.
And here `NVal` comes from user code, which we use as an upperbound: `retVal <
NVal`, which we assume `true`.
This makes me wonder if we could make them contradict and return us a null
state; which we then unconditionally dereference.
Could you have a test for like this?
```
size_t n = -1;
getline(&buffer, &n, F1); // no-crash
```
https://github.com/llvm/llvm-project/pull/83027
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
