[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Gabor Marton via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rGededa65d559d: [analyzer] StdLibraryFunctionsChecker: Add 
NotNull Arg Constraint (authored by martong).

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063

Files:
  clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
  clang/test/Analysis/std-c-library-functions-arg-constraints.c
  clang/test/Analysis/std-c-library-functions.c

Index: clang/test/Analysis/std-c-library-functions.c
===
--- clang/test/Analysis/std-c-library-functions.c
+++ clang/test/Analysis/std-c-library-functions.c
@@ -78,10 +78,13 @@
 size_t fread(void *, size_t, size_t, FILE *);
 size_t fwrite(const void *restrict, size_t, size_t, FILE *restrict);
 void test_fread_fwrite(FILE *fp, int *buf) {
+
   size_t x = fwrite(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(x <= 10); // expected-warning{{TRUE}}
+
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
+
   size_t z = fwrite(buf, sizeof(int), y, fp);
   clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
Index: clang/test/Analysis/std-c-library-functions-arg-constraints.c
===
--- clang/test/Analysis/std-c-library-functions-arg-constraints.c
+++ clang/test/Analysis/std-c-library-functions-arg-constraints.c
@@ -59,3 +59,29 @@
 (void)ret;
   }
 }
+
+typedef struct FILE FILE;
+typedef typeof(sizeof(int)) size_t;
+size_t fread(void *, size_t, size_t, FILE *);
+void test_notnull_concrete(FILE *fp) {
+  fread(0, sizeof(int), 10, fp); // \
+  // report-warning{{Function argument constraint is not satisfied}} \
+  // bugpath-warning{{Function argument constraint is not satisfied}} \
+  // bugpath-note{{Function argument constraint is not satisfied}}
+}
+void test_notnull_symbolic(FILE *fp, int *buf) {
+  fread(buf, sizeof(int), 10, fp);
+  clang_analyzer_eval(buf != 0); // \
+  // report-warning{{TRUE}} \
+  // bugpath-warning{{TRUE}} \
+  // bugpath-note{{TRUE}} \
+  // bugpath-note{{'buf' is not equal to null}}
+}
+void test_notnull_symbolic2(FILE *fp, int *buf) {
+  if (!buf) // bugpath-note{{Assuming 'buf' is null}} \
+// bugpath-note{{Taking true branch}}
+fread(buf, sizeof(int), 10, fp); // \
+// report-warning{{Function argument constraint is not satisfied}} \
+// bugpath-warning{{Function argument constraint is not satisfied}} \
+// bugpath-note{{Function argument constraint is not satisfied}}
+}
Index: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
===
--- clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
@@ -183,6 +183,29 @@
   const Summary ) const override;
   };
 
+  class NotNullConstraint : public ValueConstraint {
+using ValueConstraint::ValueConstraint;
+// This variable has a role when we negate the constraint.
+bool CannotBeNull = true;
+
+  public:
+ProgramStateRef apply(ProgramStateRef State, const CallEvent ,
+  const Summary ) const override {
+  SVal V = getArgSVal(Call, getArgNo());
+  DefinedOrUnknownSVal L = V.castAs();
+  if (!L.getAs())
+return State;
+
+  return State->assume(L, CannotBeNull);
+}
+
+ValueConstraintPtr negate() const override {
+  NotNullConstraint Tmp(*this);
+  Tmp.CannotBeNull = !this->CannotBeNull;
+  return std::make_shared(Tmp);
+}
+  };
+
   /// The complete list of constraints that defines a single branch.
   typedef std::vector ConstraintSet;
 
@@ -233,9 +256,6 @@
  "We should have had no significant void types in the spec");
   assert(T.isCanonical() &&
  "We should only have canonical types in the spec");
-  // FIXME: lift this assert (but not the ones above!)
-  assert(T->isIntegralOrEnumerationType() &&
- "We only support integral ranges in the spec");
 }
 
   public:
@@ -602,6 +622,9 @@
   const QualType LongTy = ACtx.LongTy;
   const QualType LongLongTy = ACtx.LongLongTy;
   const QualType SizeTy = ACtx.getSizeType();
+  const QualType VoidPtrTy = ACtx.VoidPtrTy; // void *T
+  const QualType ConstVoidPtrTy =
+  ACtx.getPointerType(ACtx.VoidTy.withConst()); // const void *T
 
   const RangeInt IntMax = BVF.getMaxValue(IntTy).getLimitedValue();
   const RangeInt LongMax = BVF.getMaxValue(LongTy).getLimitedValue();
@@ -672,6 +695,9 @@
 return IntRangeVector{std::pair{v, v}};
   };
   auto LessThanOrEq = BO_LE;
+  auto NotNull = [&](ArgNo ArgN) {
+return std::make_shared(ArgN);
+  };
 
   using RetType = QualType;
   // Templates for summaries that are reused by many functions.
@@ -687,11 

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D75063#1923780 , @NoQ wrote:

> This is basically a shorthand for "outside [0, 0]", right? I don't mind ^.^


Yeah, and my first attempt was exactly to implement this with ranges. However, 
it failed when I realized that we cannot cast a pointer to `NonLoc`, so the 
already written `RangeConstraint::apply*` functions could not work (I would 
have to add another branch for handling `Loc` kind of SVals for the pointer 
case).




Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:175
+using ValueConstraint::ValueConstraint;
+bool CannotBeNull = true;
+

Szelethus wrote:
> martong wrote:
> > Szelethus wrote:
> > > What does this do? Is it ever used in the patch?
> > Yes, it is used. We use it in `apply` the value is passed to `assume`.
> > And in `negate` we flip the value.
> Forgot my eyes in the office. Woops. I would still prefer a line of comment 
> here :)
Ok, I added a comment about its role.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:684
+.Case({
+ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+})

martong wrote:
> steakhal wrote:
> > Two lines below you are using the `{0U}` initialization syntax, and here 
> > the simple constructor call syntax.
> > Shouldn't we pick one?
> Yes, definitely. I think I am going to use brace initialization syntax 
> everywhere.
Finally I ended up with the parens. :)



Comment at: 
clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:889-890
   Read(LongLongTy, LongLongMax)}},
   {"fread", Summaries{Fread()}},
-  {"fwrite", Summaries{Fread()}},
+  {"fwrite", Summaries{Fwrite()}},
   // getline()-like functions either fail or read at least the delimiter.

Szelethus wrote:
> Not super relevant to this specific revision, but shouldn't we leave these to 
> `StreamChecker`?
Well, yeah we could remove `fread` and `fwrite` from the summaries entirely at 
some point, but that will require changing the test files here.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 251674.
martong marked 9 inline comments as done.
martong added a comment.

- Use report/bugpath verify prefixes in test
- Address review nits


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063

Files:
  clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
  clang/test/Analysis/std-c-library-functions-arg-constraints.c
  clang/test/Analysis/std-c-library-functions.c

Index: clang/test/Analysis/std-c-library-functions.c
===
--- clang/test/Analysis/std-c-library-functions.c
+++ clang/test/Analysis/std-c-library-functions.c
@@ -78,10 +78,13 @@
 size_t fread(void *, size_t, size_t, FILE *);
 size_t fwrite(const void *restrict, size_t, size_t, FILE *restrict);
 void test_fread_fwrite(FILE *fp, int *buf) {
+
   size_t x = fwrite(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(x <= 10); // expected-warning{{TRUE}}
+
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
+
   size_t z = fwrite(buf, sizeof(int), y, fp);
   clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
Index: clang/test/Analysis/std-c-library-functions-arg-constraints.c
===
--- clang/test/Analysis/std-c-library-functions-arg-constraints.c
+++ clang/test/Analysis/std-c-library-functions-arg-constraints.c
@@ -59,3 +59,29 @@
 (void)ret;
   }
 }
+
+typedef struct FILE FILE;
+typedef typeof(sizeof(int)) size_t;
+size_t fread(void *, size_t, size_t, FILE *);
+void test_notnull_concrete(FILE *fp) {
+  fread(0, sizeof(int), 10, fp); // \
+  // report-warning{{Function argument constraint is not satisfied}} \
+  // bugpath-warning{{Function argument constraint is not satisfied}} \
+  // bugpath-note{{Function argument constraint is not satisfied}}
+}
+void test_notnull_symbolic(FILE *fp, int *buf) {
+  fread(buf, sizeof(int), 10, fp);
+  clang_analyzer_eval(buf != 0); // \
+  // report-warning{{TRUE}} \
+  // bugpath-warning{{TRUE}} \
+  // bugpath-note{{TRUE}} \
+  // bugpath-note{{'buf' is not equal to null}}
+}
+void test_notnull_symbolic2(FILE *fp, int *buf) {
+  if (!buf) // bugpath-note{{Assuming 'buf' is null}} \
+// bugpath-note{{Taking true branch}}
+fread(buf, sizeof(int), 10, fp); // \
+// report-warning{{Function argument constraint is not satisfied}} \
+// bugpath-warning{{Function argument constraint is not satisfied}} \
+// bugpath-note{{Function argument constraint is not satisfied}}
+}
Index: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
===
--- clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
@@ -183,6 +183,29 @@
   const Summary ) const override;
   };
 
+  class NotNullConstraint : public ValueConstraint {
+using ValueConstraint::ValueConstraint;
+// This variable has a role when we negate the constraint.
+bool CannotBeNull = true;
+
+  public:
+ProgramStateRef apply(ProgramStateRef State, const CallEvent ,
+  const Summary ) const override {
+  SVal V = getArgSVal(Call, getArgNo());
+  DefinedOrUnknownSVal L = V.castAs();
+  if (!L.getAs())
+return State;
+
+  return State->assume(L, CannotBeNull);
+}
+
+ValueConstraintPtr negate() const override {
+  NotNullConstraint Tmp(*this);
+  Tmp.CannotBeNull = !this->CannotBeNull;
+  return std::make_shared(Tmp);
+}
+  };
+
   /// The complete list of constraints that defines a single branch.
   typedef std::vector ConstraintSet;
 
@@ -233,9 +256,6 @@
  "We should have had no significant void types in the spec");
   assert(T.isCanonical() &&
  "We should only have canonical types in the spec");
-  // FIXME: lift this assert (but not the ones above!)
-  assert(T->isIntegralOrEnumerationType() &&
- "We only support integral ranges in the spec");
 }
 
   public:
@@ -602,6 +622,9 @@
   const QualType LongTy = ACtx.LongTy;
   const QualType LongLongTy = ACtx.LongLongTy;
   const QualType SizeTy = ACtx.getSizeType();
+  const QualType VoidPtrTy = ACtx.VoidPtrTy; // void *T
+  const QualType ConstVoidPtrTy =
+  ACtx.getPointerType(ACtx.VoidTy.withConst()); // const void *T
 
   const RangeInt IntMax = BVF.getMaxValue(IntTy).getLimitedValue();
   const RangeInt LongMax = BVF.getMaxValue(LongTy).getLimitedValue();
@@ -672,6 +695,9 @@
 return IntRangeVector{std::pair{v, v}};
   };
   auto LessThanOrEq = BO_LE;
+  auto NotNull = [&](ArgNo ArgN) {
+return std::make_shared(ArgN);
+  };
 
   using RetType = QualType;
   // Templates for summaries that are reused by many functions.
@@ -687,11 +713,20 @@
 

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Kristóf Umann via Phabricator via cfe-commits]

Szelethus accepted this revision.
Szelethus added a comment.

LGTM! Please address the nits before commiting, but there is no need for 
another round of reviews. :)

edit: from my end, that is.




Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:175
+using ValueConstraint::ValueConstraint;
+bool CannotBeNull = true;
+

martong wrote:
> Szelethus wrote:
> > What does this do? Is it ever used in the patch?
> Yes, it is used. We use it in `apply` the value is passed to `assume`.
> And in `negate` we flip the value.
Forgot my eyes in the office. Woops. I would still prefer a line of comment 
here :)



Comment at: 
clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:889-890
   Read(LongLongTy, LongLongMax)}},
   {"fread", Summaries{Fread()}},
-  {"fwrite", Summaries{Fread()}},
+  {"fwrite", Summaries{Fwrite()}},
   // getline()-like functions either fail or read at least the delimiter.

Not super relevant to this specific revision, but shouldn't we leave these to 
`StreamChecker`?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Gabor Marton via Phabricator via cfe-commits]

martong marked 6 inline comments as done.
martong added inline comments.
Herald added a subscriber: ASDenysPetrov.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:175
+using ValueConstraint::ValueConstraint;
+bool CannotBeNull = true;
+

Szelethus wrote:
> What does this do? Is it ever used in the patch?
Yes, it is used. We use it in `apply` the value is passed to `assume`.
And in `negate` we flip the value.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:189
+ValueConstraintPtr negate() const override {
+  NotNullConstraint tmp(*this);
+  tmp.CannotBeNull = !this->CannotBeNull;

balazske wrote:
> Is `Tmp` better name?
Absolutely, yes, I should avoid lower case variables, will rename.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:684
+.Case({
+ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+})

steakhal wrote:
> Two lines below you are using the `{0U}` initialization syntax, and here the 
> simple constructor call syntax.
> Shouldn't we pick one?
Yes, definitely. I think I am going to use brace initialization syntax 
everywhere.



Comment at: clang/test/Analysis/std-c-library-functions-arg-constraints.c:59
+fread(buf, sizeof(int), 10, fp); // expected-warning{{Function argument 
constraint is not satisfied}}
+}

balazske wrote:
> One difficulty is that `fread` can work if the `buf` is 0 and `count` is 0 
> too. There is for sure code that uses this feature.
My understanding is that in case of `fread`, if `buf` is 0 then that is an 
undefined behavior.

In the section in C11 describing the use of library functions (§7.1.4) it is 
stated that:



> If an argument to a function has an invalid value (such as a value outside 
> the domain of the function, or a pointer outside the address space of the 
> program, or a null pointer, or a pointer to non-modifiable storage when the 
> corresponding parameter is not const-qualified) or a type (after promotion) 
> not expected by a function with variable number of arguments, the behavior is 
> undefined. If a function argument is described as being an array, the pointer 
> actually passed to the function shall have a value such that all address 
> computations and accesses to objects (that would be valid if the pointer did 
> point to the first element of such an array) are in fact valid.

I've found more details in this StackOverflow post:
https://stackoverflow.com/questions/51779960/is-it-safe-to-fread-0-bytes-into-a-null-pointer

Also note that a sane libc implementation would not dereference `buf` if `size` 
is 0, but we may not rely on these implementation details, that is why this is 
declared as undefined behavior in the standard.




Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Balázs Kéri via Phabricator via cfe-commits]

balazske added inline comments.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:189
+ValueConstraintPtr negate() const override {
+  NotNullConstraint tmp(*this);
+  tmp.CannotBeNull = !this->CannotBeNull;

Is `Tmp` better name?



Comment at: clang/test/Analysis/std-c-library-functions-arg-constraints.c:59
+fread(buf, sizeof(int), 10, fp); // expected-warning{{Function argument 
constraint is not satisfied}}
+}

One difficulty is that `fread` can work if the `buf` is 0 and `count` is 0 too. 
There is for sure code that uses this feature.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Artem Dergachev via Phabricator via cfe-commits]

NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.

This is basically a shorthand for "outside [0, 0]", right? I don't mind ^.^


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Kristóf Umann via Phabricator via cfe-commits]

Szelethus added inline comments.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:175
+using ValueConstraint::ValueConstraint;
+bool CannotBeNull = true;
+

What does this do? Is it ever used in the patch?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Balázs Benics via Phabricator via cfe-commits]

steakhal added inline comments.



Comment at: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp:684
+.Case({
+ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+})

Two lines below you are using the `{0U}` initialization syntax, and here the 
simple constructor call syntax.
Shouldn't we pick one?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75063/new/

https://reviews.llvm.org/D75063



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D75063: [analyzer] StdLibraryFunctionsChecker: Add NotNull Arg Constraint

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: NoQ, Szelethus, balazske, gamesh411, 
baloghadamsoftware, steakhal.
Herald added subscribers: cfe-commits, Charusso, dkrupp, donat.nagy, 
mikhail.ramalho, a.sidorin, rnkovacs, szepet, xazax.hun, whisperity.
Herald added a project: clang.
martong added a parent revision: D73898: [analyzer] StdLibraryFunctionsChecker: 
Add argument constraints.

Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D75063

Files:
  clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
  clang/test/Analysis/std-c-library-functions-arg-constraints.c
  clang/test/Analysis/std-c-library-functions.c

Index: clang/test/Analysis/std-c-library-functions.c
===
--- clang/test/Analysis/std-c-library-functions.c
+++ clang/test/Analysis/std-c-library-functions.c
@@ -78,10 +78,13 @@
 size_t fread(void *, size_t, size_t, FILE *);
 size_t fwrite(const void *restrict, size_t, size_t, FILE *restrict);
 void test_fread_fwrite(FILE *fp, int *buf) {
+
   size_t x = fwrite(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(x <= 10); // expected-warning{{TRUE}}
+
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
+
   size_t z = fwrite(buf, sizeof(int), y, fp);
   clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
Index: clang/test/Analysis/std-c-library-functions-arg-constraints.c
===
--- clang/test/Analysis/std-c-library-functions-arg-constraints.c
+++ clang/test/Analysis/std-c-library-functions-arg-constraints.c
@@ -42,3 +42,18 @@
 
   ret = x / y; // expected-warning{{Division by zero}}
 }
+
+typedef struct FILE FILE;
+typedef typeof(sizeof(int)) size_t;
+size_t fread(void *, size_t, size_t, FILE *);
+void test_notnull_concrete(FILE *fp) {
+  fread(0, sizeof(int), 10, fp); // expected-warning{{Function argument constraint is not satisfied}}
+}
+void test_notnull_symbolic(FILE *fp, int *buf) {
+  fread(buf, sizeof(int), 10, fp);
+  clang_analyzer_eval(buf != 0); // expected-warning{{TRUE}}
+}
+void test_notnull_symbolic2(FILE *fp, int *buf) {
+  if (!buf)
+fread(buf, sizeof(int), 10, fp); // expected-warning{{Function argument constraint is not satisfied}}
+}
Index: clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
===
--- clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
@@ -170,6 +170,28 @@
   const Summary ) const override;
   };
 
+  class NotNullConstraint : public ValueConstraint {
+using ValueConstraint::ValueConstraint;
+bool CannotBeNull = true;
+
+  public:
+ProgramStateRef apply(ProgramStateRef State, const CallEvent ,
+  const Summary ) const override {
+  SVal V = getArgSVal(Call, getArgNo());
+  DefinedOrUnknownSVal L = V.castAs();
+  if (!L.getAs())
+return State;
+
+  return State->assume(L, CannotBeNull);
+}
+
+ValueConstraintPtr negate() const override {
+  NotNullConstraint tmp(*this);
+  tmp.CannotBeNull = !this->CannotBeNull;
+  return std::make_shared(tmp);
+}
+  };
+
   /// The complete list of constraints that defines a single branch.
   typedef std::vector ConstraintSet;
 
@@ -210,9 +232,6 @@
  "We should have had no significant void types in the spec");
   assert(T.isCanonical() &&
  "We should only have canonical types in the spec");
-  // FIXME: lift this assert (but not the ones above!)
-  assert(T->isIntegralOrEnumerationType() &&
- "We only support integral ranges in the spec");
 }
 
   public:
@@ -574,6 +593,9 @@
   const QualType LongTy = ACtx.LongTy;
   const QualType LongLongTy = ACtx.LongLongTy;
   const QualType SizeTy = ACtx.getSizeType();
+  const QualType VoidPtrTy = ACtx.VoidPtrTy; // void *T
+  const QualType ConstVoidPtrTy =
+  ACtx.getPointerType(ACtx.VoidTy.withConst()); // const void *T
 
   const RangeInt IntMax = BVF.getMaxValue(IntTy).getLimitedValue();
   const RangeInt LongMax = BVF.getMaxValue(LongTy).getLimitedValue();
@@ -638,6 +660,9 @@
 return IntRangeVector{std::pair{v, v}};
   };
   auto LessThanOrEq = BO_LE;
+  auto NotNull = [&](ArgNo ArgN) {
+return std::make_shared(ArgN);
+  };
 
   using RetType = QualType;
   // Templates for summaries that are reused by many functions.
@@ -653,11 +678,20 @@
ReturnValueCondition(WithinRange, Range(-1, Max))});
   };
   auto Fread = [&]() {
-return Summary(ArgTypes{Irrelevant, Irrelevant, SizeTy, Irrelevant},
+return Summary(ArgTypes{VoidPtrTy, Irrelevant, SizeTy, Irrelevant},
+   RetType{SizeTy}, NoEvalCall)
+.Case({
+ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+})
+