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

Reply via email to