1 files changed, 1403 insertions, 655 deletions

diff --git a/contrib/llvm-project/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp b/contrib/llvm-project/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
index 8b575f4f4759..d1c366a94fac 100644
--- a/contrib/llvm-project/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
+++ b/contrib/llvm-project/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
@@ -40,12 +40,12 @@
 //
 // The following standard C functions are currently supported:
 //
-//   fgetc      getline   isdigit   isupper
+//   fgetc      getline   isdigit   isupper     toascii
 //   fread      isalnum   isgraph   isxdigit
 //   fwrite     isalpha   islower   read
 //   getc       isascii   isprint   write
-//   getchar    isblank   ispunct
-//   getdelim   iscntrl   isspace
+//   getchar    isblank   ispunct   toupper
+//   getdelim   iscntrl   isspace   tolower
 //
 //===----------------------------------------------------------------------===//
 
@@ -126,6 +126,8 @@ class StdLibraryFunctionsChecker
     }
     ArgNo getArgNo() const { return ArgN; }
 
+    virtual StringRef getName() const = 0;
+
   protected:
     ArgNo ArgN; // Argument to which we apply the constraint.
 
@@ -138,18 +140,25 @@ class StdLibraryFunctionsChecker
   /// Given a range, should the argument stay inside or outside this range?
   enum RangeKind { OutOfRange, WithinRange };
 
-  /// Encapsulates a single range on a single symbol within a branch.
+  /// Encapsulates a range on a single symbol.
   class RangeConstraint : public ValueConstraint {
-    RangeKind Kind;      // Kind of range definition.
-    IntRangeVector Args; // Polymorphic arguments.
+    RangeKind Kind;
+    // A range is formed as a set of intervals (sub-ranges).
+    // E.g. {['A', 'Z'], ['a', 'z']}
+    //
+    // The default constructed RangeConstraint has an empty range set, applying
+    // such constraint does not involve any assumptions, thus the State remains
+    // unchanged. This is meaningful, if the range is dependent on a looked up
+    // type (e.g. [0, Socklen_tMax]). If the type is not found, then the range
+    // is default initialized to be empty.
+    IntRangeVector Ranges;
 
   public:
-    RangeConstraint(ArgNo ArgN, RangeKind Kind, const IntRangeVector &Args)
-        : ValueConstraint(ArgN), Kind(Kind), Args(Args) {}
+    StringRef getName() const override { return "Range"; }
+    RangeConstraint(ArgNo ArgN, RangeKind Kind, const IntRangeVector &Ranges)
+        : ValueConstraint(ArgN), Kind(Kind), Ranges(Ranges) {}
 
-    const IntRangeVector &getRanges() const {
-      return Args;
-    }
+    const IntRangeVector &getRanges() const { return Ranges; }
 
   private:
     ProgramStateRef applyAsOutOfRange(ProgramStateRef State,
@@ -158,6 +167,7 @@ class StdLibraryFunctionsChecker
     ProgramStateRef applyAsWithinRange(ProgramStateRef State,
                                        const CallEvent &Call,
                                        const Summary &Summary) const;
+
   public:
     ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
                           const Summary &Summary,
@@ -198,6 +208,7 @@ class StdLibraryFunctionsChecker
     ArgNo OtherArgN;
 
   public:
+    virtual StringRef getName() const override { return "Comparison"; };
     ComparisonConstraint(ArgNo ArgN, BinaryOperator::Opcode Opcode,
                          ArgNo OtherArgN)
         : ValueConstraint(ArgN), Opcode(Opcode), OtherArgN(OtherArgN) {}
@@ -214,6 +225,7 @@ class StdLibraryFunctionsChecker
     bool CannotBeNull = true;
 
   public:
+    StringRef getName() const override { return "NonNull"; }
     ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
                           const Summary &Summary,
                           CheckerContext &C) const override {
@@ -242,15 +254,21 @@ class StdLibraryFunctionsChecker
     }
   };
 
-  // Represents a buffer argument with an additional size argument.
-  // E.g. the first two arguments here:
+  // Represents a buffer argument with an additional size constraint. The
+  // constraint may be a concrete value, or a symbolic value in an argument.
+  // Example 1. Concrete value as the minimum buffer size.
+  //   char *asctime_r(const struct tm *restrict tm, char *restrict buf);
+  //   // `buf` size must be at least 26 bytes according the POSIX standard.
+  // Example 2. Argument as a buffer size.
   //   ctime_s(char *buffer, rsize_t bufsz, const time_t *time);
-  // Another example:
+  // Example 3. The size is computed as a multiplication of other args.
   //   size_t fread(void *ptr, size_t size, size_t nmemb, FILE *stream);
   //   // Here, ptr is the buffer, and its minimum size is `size * nmemb`.
   class BufferSizeConstraint : public ValueConstraint {
+    // The concrete value which is the minimum size for the buffer.
+    llvm::Optional<llvm::APSInt> ConcreteSize;
     // The argument which holds the size of the buffer.
-    ArgNo SizeArgN;
+    llvm::Optional<ArgNo> SizeArgN;
     // The argument which is a multiplier to size. This is set in case of
     // `fread` like functions where the size is computed as a multiplication of
     // two arguments.
@@ -259,9 +277,11 @@ class StdLibraryFunctionsChecker
     BinaryOperator::Opcode Op = BO_LE;
 
   public:
+    StringRef getName() const override { return "BufferSize"; }
+    BufferSizeConstraint(ArgNo Buffer, llvm::APSInt BufMinSize)
+        : ValueConstraint(Buffer), ConcreteSize(BufMinSize) {}
     BufferSizeConstraint(ArgNo Buffer, ArgNo BufSize)
         : ValueConstraint(Buffer), SizeArgN(BufSize) {}
-
     BufferSizeConstraint(ArgNo Buffer, ArgNo BufSize, ArgNo BufSizeMultiplier)
         : ValueConstraint(Buffer), SizeArgN(BufSize),
           SizeMultiplierArgN(BufSizeMultiplier) {}
@@ -272,14 +292,27 @@ class StdLibraryFunctionsChecker
       SValBuilder &SvalBuilder = C.getSValBuilder();
       // The buffer argument.
       SVal BufV = getArgSVal(Call, getArgNo());
-      // The size argument.
-      SVal SizeV = getArgSVal(Call, SizeArgN);
-      // Multiply with another argument if given.
-      if (SizeMultiplierArgN) {
-        SVal SizeMulV = getArgSVal(Call, *SizeMultiplierArgN);
-        SizeV = SvalBuilder.evalBinOp(State, BO_Mul, SizeV, SizeMulV,
-                                      Summary.getArgType(SizeArgN));
-      }
+
+      // Get the size constraint.
+      const SVal SizeV = [this, &State, &Call, &Summary, &SvalBuilder]() {
+        if (ConcreteSize) {
+          return SVal(SvalBuilder.makeIntVal(*ConcreteSize));
+        } else if (SizeArgN) {
+          // The size argument.
+          SVal SizeV = getArgSVal(Call, *SizeArgN);
+          // Multiply with another argument if given.
+          if (SizeMultiplierArgN) {
+            SVal SizeMulV = getArgSVal(Call, *SizeMultiplierArgN);
+            SizeV = SvalBuilder.evalBinOp(State, BO_Mul, SizeV, SizeMulV,
+                                          Summary.getArgType(*SizeArgN));
+          }
+          return SizeV;
+        } else {
+          llvm_unreachable("The constraint must be either a concrete value or "
+                           "encoded in an arguement.");
+        }
+      }();
+
       // The dynamic size of the buffer argument, got from the analyzer engine.
       SVal BufDynSize = getDynamicSizeWithOffset(State, BufV);
 
@@ -302,12 +335,20 @@ class StdLibraryFunctionsChecker
       Tmp.Op = BinaryOperator::negateComparisonOp(Op);
       return std::make_shared<BufferSizeConstraint>(Tmp);
     }
+
+    bool checkSpecificValidity(const FunctionDecl *FD) const override {
+      const bool ValidArg = getArgType(FD, ArgN)->isPointerType();
+      assert(ValidArg &&
+             "This constraint should be applied only on a pointer type");
+      return ValidArg;
+    }
   };
 
   /// The complete list of constraints that defines a single branch.
   typedef std::vector<ValueConstraintPtr> ConstraintSet;
 
-  using ArgTypes = std::vector<QualType>;
+  using ArgTypes = std::vector<Optional<QualType>>;
+  using RetType = Optional<QualType>;
 
   // A placeholder type, we use it whenever we do not care about the concrete
   // type in a Signature.
@@ -317,16 +358,37 @@ class StdLibraryFunctionsChecker
   // The signature of a function we want to describe with a summary. This is a
   // concessive signature, meaning there may be irrelevant types in the
   // signature which we do not check against a function with concrete types.
-  struct Signature {
-    const ArgTypes ArgTys;
-    const QualType RetTy;
-    Signature(ArgTypes ArgTys, QualType RetTy) : ArgTys(ArgTys), RetTy(RetTy) {
-      assertRetTypeSuitableForSignature(RetTy);
-      for (size_t I = 0, E = ArgTys.size(); I != E; ++I) {
-        QualType ArgTy = ArgTys[I];
-        assertArgTypeSuitableForSignature(ArgTy);
+  // All types in the spec need to be canonical.
+  class Signature {
+    using ArgQualTypes = std::vector<QualType>;
+    ArgQualTypes ArgTys;
+    QualType RetTy;
+    // True if any component type is not found by lookup.
+    bool Invalid = false;
+
+  public:
+    // Construct a signature from optional types. If any of the optional types
+    // are not set then the signature will be invalid.
+    Signature(ArgTypes ArgTys, RetType RetTy) {
+      for (Optional<QualType> Arg : ArgTys) {
+        if (!Arg) {
+          Invalid = true;
+          return;
+        } else {
+          assertArgTypeSuitableForSignature(*Arg);
+          this->ArgTys.push_back(*Arg);
+        }
+      }
+      if (!RetTy) {
+        Invalid = true;
+        return;
+      } else {
+        assertRetTypeSuitableForSignature(*RetTy);
+        this->RetTy = *RetTy;
       }
     }
+
+    bool isInvalid() const { return Invalid; }
     bool matches(const FunctionDecl *FD) const;
 
   private:
@@ -380,7 +442,6 @@ class StdLibraryFunctionsChecker
   ///   rules for the given parameter's type, those rules are checked once the
   ///   signature is matched.
   class Summary {
-    const Signature Sign;
     const InvalidationKind InvalidationKd;
     Cases CaseConstraints;
     ConstraintSet ArgConstraints;
@@ -390,14 +451,19 @@ class StdLibraryFunctionsChecker
     const FunctionDecl *FD = nullptr;
 
   public:
-    Summary(ArgTypes ArgTys, QualType RetTy, InvalidationKind InvalidationKd)
-        : Sign(ArgTys, RetTy), InvalidationKd(InvalidationKd) {}
+    Summary(InvalidationKind InvalidationKd) : InvalidationKd(InvalidationKd) {}
 
-    Summary &Case(ConstraintSet&& CS) {
+    Summary &Case(ConstraintSet &&CS) {
       CaseConstraints.push_back(std::move(CS));
       return *this;
     }
+    Summary &Case(const ConstraintSet &CS) {
+      CaseConstraints.push_back(CS);
+      return *this;
+    }
     Summary &ArgConstraint(ValueConstraintPtr VC) {
+      assert(VC->getArgNo() != Ret &&
+             "Arg constraint should not refer to the return value");
       ArgConstraints.push_back(VC);
       return *this;
     }
@@ -412,7 +478,7 @@ class StdLibraryFunctionsChecker
 
     // Returns true if the summary should be applied to the given function.
     // And if yes then store the function declaration.
-    bool matchesAndSet(const FunctionDecl *FD) {
+    bool matchesAndSet(const Signature &Sign, const FunctionDecl *FD) {
       bool Result = Sign.matches(FD) && validateByConstraints(FD);
       if (Result) {
         assert(!this->FD && "FD must not be set more than once");
@@ -472,17 +538,24 @@ private:
   void initFunctionSummaries(CheckerContext &C) const;
 
   void reportBug(const CallEvent &Call, ExplodedNode *N,
-                 CheckerContext &C) const {
+                 const ValueConstraint *VC, CheckerContext &C) const {
     if (!ChecksEnabled[CK_StdCLibraryFunctionArgsChecker])
       return;
-    // TODO Add detailed diagnostic.
-    StringRef Msg = "Function argument constraint is not satisfied";
+    // TODO Add more detailed diagnostic.
+    std::string Msg =
+        (Twine("Function argument constraint is not satisfied, constraint: ") +
+         VC->getName().data() + ", ArgN: " + Twine(VC->getArgNo()))
+            .str();
     if (!BT_InvalidArg)
       BT_InvalidArg = std::make_unique<BugType>(
           CheckNames[CK_StdCLibraryFunctionArgsChecker],
           "Unsatisfied argument constraints", categories::LogicError);
     auto R = std::make_unique<PathSensitiveBugReport>(*BT_InvalidArg, Msg, N);
-    bugreporter::trackExpressionValue(N, Call.getArgExpr(0), *R);
+    bugreporter::trackExpressionValue(N, Call.getArgExpr(VC->getArgNo()), *R);
+
+    // Highlight the range of the argument that was violated.
+    R->addRange(Call.getArgSourceRange(VC->getArgNo()));
+
     C.emitReport(std::move(R));
   }
 };
@@ -495,6 +568,8 @@ const StdLibraryFunctionsChecker::ArgNo StdLibraryFunctionsChecker::Ret =
 ProgramStateRef StdLibraryFunctionsChecker::RangeConstraint::applyAsOutOfRange(
     ProgramStateRef State, const CallEvent &Call,
     const Summary &Summary) const {
+  if (Ranges.empty())
+    return State;
 
   ProgramStateManager &Mgr = State->getStateManager();
   SValBuilder &SVB = Mgr.getSValBuilder();
@@ -522,6 +597,8 @@ ProgramStateRef StdLibraryFunctionsChecker::RangeConstraint::applyAsOutOfRange(
 ProgramStateRef StdLibraryFunctionsChecker::RangeConstraint::applyAsWithinRange(
     ProgramStateRef State, const CallEvent &Call,
     const Summary &Summary) const {
+  if (Ranges.empty())
+    return State;
 
   ProgramStateManager &Mgr = State->getStateManager();
   SValBuilder &SVB = Mgr.getSValBuilder();
@@ -615,7 +692,7 @@ void StdLibraryFunctionsChecker::checkPreCall(const CallEvent &Call,
     // The argument constraint is not satisfied.
     if (FailureSt && !SuccessSt) {
       if (ExplodedNode *N = C.generateErrorNode(NewState))
-        reportBug(Call, N, C);
+        reportBug(Call, N, Constraint.get(), C);
       break;
     } else {
       // We will apply the constraint even if we cannot reason about the
@@ -665,7 +742,7 @@ bool StdLibraryFunctionsChecker::evalCall(const CallEvent &Call,
   case EvalCallAsPure: {
     ProgramStateRef State = C.getState();
     const LocationContext *LC = C.getLocationContext();
-    const auto *CE = cast_or_null<CallExpr>(Call.getOriginExpr());
+    const auto *CE = cast<CallExpr>(Call.getOriginExpr());
     SVal V = C.getSValBuilder().conjureSymbolVal(
         CE, LC, CE->getType().getCanonicalType(), C.blockCount());
     State = State->BindExpr(CE, LC, V);
@@ -682,21 +759,39 @@ bool StdLibraryFunctionsChecker::evalCall(const CallEvent &Call,
 
 bool StdLibraryFunctionsChecker::Signature::matches(
     const FunctionDecl *FD) const {
-  // Check number of arguments:
+  assert(!isInvalid());
+  // Check the number of arguments.
   if (FD->param_size() != ArgTys.size())
     return false;
 
-  // Check return type.
-  if (!isIrrelevant(RetTy))
-    if (RetTy != FD->getReturnType().getCanonicalType())
+  // The "restrict" keyword is illegal in C++, however, many libc
+  // implementations use the "__restrict" compiler intrinsic in functions
+  // prototypes. The "__restrict" keyword qualifies a type as a restricted type
+  // even in C++.
+  // In case of any non-C99 languages, we don't want to match based on the
+  // restrict qualifier because we cannot know if the given libc implementation
+  // qualifies the paramter type or not.
+  auto RemoveRestrict = [&FD](QualType T) {
+    if (!FD->getASTContext().getLangOpts().C99)
+      T.removeLocalRestrict();
+    return T;
+  };
+
+  // Check the return type.
+  if (!isIrrelevant(RetTy)) {
+    QualType FDRetTy = RemoveRestrict(FD->getReturnType().getCanonicalType());
+    if (RetTy != FDRetTy)
       return false;
+  }
 
-  // Check argument types.
+  // Check the argument types.
   for (size_t I = 0, E = ArgTys.size(); I != E; ++I) {
     QualType ArgTy = ArgTys[I];
     if (isIrrelevant(ArgTy))
       continue;
-    if (ArgTy != FD->getParamDecl(I)->getType().getCanonicalType())
+    QualType FDArgTy =
+        RemoveRestrict(FD->getParamDecl(I)->getType().getCanonicalType());
+    if (ArgTy != FDArgTy)
       return false;
   }
 
@@ -726,32 +821,6 @@ StdLibraryFunctionsChecker::findFunctionSummary(const CallEvent &Call,
   return findFunctionSummary(FD, C);
 }
 
-static llvm::Optional<QualType> lookupType(StringRef Name,
-                                           const ASTContext &ACtx) {
-  IdentifierInfo &II = ACtx.Idents.get(Name);
-  auto LookupRes = ACtx.getTranslationUnitDecl()->lookup(&II);
-  if (LookupRes.size() == 0)
-    return None;
-
-  // Prioritze typedef declarations.
-  // This is needed in case of C struct typedefs. E.g.:
-  //   typedef struct FILE FILE;
-  // In this case, we have a RecordDecl 'struct FILE' with the name 'FILE' and
-  // we have a TypedefDecl with the name 'FILE'.
-  for (Decl *D : LookupRes)
-    if (auto *TD = dyn_cast<TypedefNameDecl>(D))
-      return ACtx.getTypeDeclType(TD).getCanonicalType();
-
-  // Find the first TypeDecl.
-  // There maybe cases when a function has the same name as a struct.
-  // E.g. in POSIX: `struct stat` and the function `stat()`:
-  //   int stat(const char *restrict path, struct stat *restrict buf);
-  for (Decl *D : LookupRes)
-    if (auto *TD = dyn_cast<TypeDecl>(D))
-      return ACtx.getTypeDeclType(TD).getCanonicalType();
-  return None;
-}
-
 void StdLibraryFunctionsChecker::initFunctionSummaries(
     CheckerContext &C) const {
   if (!FunctionSummaryMap.empty())
@@ -761,6 +830,91 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
   BasicValueFactory &BVF = SVB.getBasicValueFactory();
   const ASTContext &ACtx = BVF.getContext();
 
+  // Helper class to lookup a type by its name.
+  class LookupType {
+    const ASTContext &ACtx;
+
+  public:
+    LookupType(const ASTContext &ACtx) : ACtx(ACtx) {}
+
+    // Find the type. If not found then the optional is not set.
+    llvm::Optional<QualType> operator()(StringRef Name) {
+      IdentifierInfo &II = ACtx.Idents.get(Name);
+      auto LookupRes = ACtx.getTranslationUnitDecl()->lookup(&II);
+      if (LookupRes.size() == 0)
+        return None;
+
+      // Prioritze typedef declarations.
+      // This is needed in case of C struct typedefs. E.g.:
+      //   typedef struct FILE FILE;
+      // In this case, we have a RecordDecl 'struct FILE' with the name 'FILE'
+      // and we have a TypedefDecl with the name 'FILE'.
+      for (Decl *D : LookupRes)
+        if (auto *TD = dyn_cast<TypedefNameDecl>(D))
+          return ACtx.getTypeDeclType(TD).getCanonicalType();
+
+      // Find the first TypeDecl.
+      // There maybe cases when a function has the same name as a struct.
+      // E.g. in POSIX: `struct stat` and the function `stat()`:
+      //   int stat(const char *restrict path, struct stat *restrict buf);
+      for (Decl *D : LookupRes)
+        if (auto *TD = dyn_cast<TypeDecl>(D))
+          return ACtx.getTypeDeclType(TD).getCanonicalType();
+      return None;
+    }
+  } lookupTy(ACtx);
+
+  // Below are auxiliary classes to handle optional types that we get as a
+  // result of the lookup.
+  class GetRestrictTy {
+    const ASTContext &ACtx;
+
+  public:
+    GetRestrictTy(const ASTContext &ACtx) : ACtx(ACtx) {}
+    QualType operator()(QualType Ty) {
+      return ACtx.getLangOpts().C99 ? ACtx.getRestrictType(Ty) : Ty;
+    }
+    Optional<QualType> operator()(Optional<QualType> Ty) {
+      if (Ty)
+        return operator()(*Ty);
+      return None;
+    }
+  } getRestrictTy(ACtx);
+  class GetPointerTy {
+    const ASTContext &ACtx;
+
+  public:
+    GetPointerTy(const ASTContext &ACtx) : ACtx(ACtx) {}
+    QualType operator()(QualType Ty) { return ACtx.getPointerType(Ty); }
+    Optional<QualType> operator()(Optional<QualType> Ty) {
+      if (Ty)
+        return operator()(*Ty);
+      return None;
+    }
+  } getPointerTy(ACtx);
+  class {
+  public:
+    Optional<QualType> operator()(Optional<QualType> Ty) {
+      return Ty ? Optional<QualType>(Ty->withConst()) : None;
+    }
+    QualType operator()(QualType Ty) { return Ty.withConst(); }
+  } getConstTy;
+  class GetMaxValue {
+    BasicValueFactory &BVF;
+
+  public:
+    GetMaxValue(BasicValueFactory &BVF) : BVF(BVF) {}
+    Optional<RangeInt> operator()(QualType Ty) {
+      return BVF.getMaxValue(Ty).getLimitedValue();
+    }
+    Optional<RangeInt> operator()(Optional<QualType> Ty) {
+      if (Ty) {
+        return operator()(*Ty);
+      }
+      return None;
+    }
+  } getMaxValue(BVF);
+
   // These types are useful for writing specifications quickly,
   // New specifications should probably introduce more types.
   // Some types are hard to obtain from the AST, eg. "ssize_t".
@@ -769,44 +923,36 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
   // or long long, so three summary variants would be enough).
   // Of course, function variants are also useful for C++ overloads.
   const QualType VoidTy = ACtx.VoidTy;
+  const QualType CharTy = ACtx.CharTy;
+  const QualType WCharTy = ACtx.WCharTy;
   const QualType IntTy = ACtx.IntTy;
   const QualType UnsignedIntTy = ACtx.UnsignedIntTy;
   const QualType LongTy = ACtx.LongTy;
-  const QualType LongLongTy = ACtx.LongLongTy;
   const QualType SizeTy = ACtx.getSizeType();
 
-  const QualType VoidPtrTy = ACtx.VoidPtrTy; // void *
-  const QualType IntPtrTy = ACtx.getPointerType(IntTy); // int *
+  const QualType VoidPtrTy = getPointerTy(VoidTy); // void *
+  const QualType IntPtrTy = getPointerTy(IntTy);   // int *
   const QualType UnsignedIntPtrTy =
-      ACtx.getPointerType(UnsignedIntTy); // unsigned int *
-  const QualType VoidPtrRestrictTy =
-      ACtx.getLangOpts().C99 ? ACtx.getRestrictType(VoidPtrTy) // void *restrict
-                             : VoidPtrTy;
+      getPointerTy(UnsignedIntTy); // unsigned int *
+  const QualType VoidPtrRestrictTy = getRestrictTy(VoidPtrTy);
   const QualType ConstVoidPtrTy =
-      ACtx.getPointerType(ACtx.VoidTy.withConst()); // const void *
-  const QualType CharPtrTy = ACtx.getPointerType(ACtx.CharTy); // char *
-  const QualType CharPtrRestrictTy =
-      ACtx.getLangOpts().C99 ? ACtx.getRestrictType(CharPtrTy) // char *restrict
-                             : CharPtrTy;
+      getPointerTy(getConstTy(VoidTy));            // const void *
+  const QualType CharPtrTy = getPointerTy(CharTy); // char *
+  const QualType CharPtrRestrictTy = getRestrictTy(CharPtrTy);
   const QualType ConstCharPtrTy =
-      ACtx.getPointerType(ACtx.CharTy.withConst()); // const char *
-  const QualType ConstCharPtrRestrictTy =
-      ACtx.getLangOpts().C99
-          ? ACtx.getRestrictType(ConstCharPtrTy) // const char *restrict
-          : ConstCharPtrTy;
-  const QualType Wchar_tPtrTy = ACtx.getPointerType(ACtx.WCharTy); // wchar_t *
+      getPointerTy(getConstTy(CharTy)); // const char *
+  const QualType ConstCharPtrRestrictTy = getRestrictTy(ConstCharPtrTy);
+  const QualType Wchar_tPtrTy = getPointerTy(WCharTy); // wchar_t *
   const QualType ConstWchar_tPtrTy =
-      ACtx.getPointerType(ACtx.WCharTy.withConst()); // const wchar_t *
-  const QualType ConstVoidPtrRestrictTy =
-      ACtx.getLangOpts().C99
-          ? ACtx.getRestrictType(ConstVoidPtrTy) // const void *restrict
-          : ConstVoidPtrTy;
+      getPointerTy(getConstTy(WCharTy)); // const wchar_t *
+  const QualType ConstVoidPtrRestrictTy = getRestrictTy(ConstVoidPtrTy);
+  const QualType SizePtrTy = getPointerTy(SizeTy);
+  const QualType SizePtrRestrictTy = getRestrictTy(SizePtrTy);
 
   const RangeInt IntMax = BVF.getMaxValue(IntTy).getLimitedValue();
   const RangeInt UnsignedIntMax =
       BVF.getMaxValue(UnsignedIntTy).getLimitedValue();
   const RangeInt LongMax = BVF.getMaxValue(LongTy).getLimitedValue();
-  const RangeInt LongLongMax = BVF.getMaxValue(LongLongTy).getLimitedValue();
   const RangeInt SizeMax = BVF.getMaxValue(SizeTy).getLimitedValue();
 
   // Set UCharRangeMax to min of int or uchar maximum value.
@@ -840,15 +986,19 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
     // Add a summary to a FunctionDecl found by lookup. The lookup is performed
     // by the given Name, and in the global scope. The summary will be attached
     // to the found FunctionDecl only if the signatures match.
-    void operator()(StringRef Name, Summary S) {
+    //
+    // Returns true if the summary has been added, false otherwise.
+    bool operator()(StringRef Name, Signature Sign, Summary Sum) {
+      if (Sign.isInvalid())
+        return false;
       IdentifierInfo &II = ACtx.Idents.get(Name);
       auto LookupRes = ACtx.getTranslationUnitDecl()->lookup(&II);
       if (LookupRes.size() == 0)
-        return;
+        return false;
       for (Decl *D : LookupRes) {
         if (auto *FD = dyn_cast<FunctionDecl>(D)) {
-          if (S.matchesAndSet(FD)) {
-            auto Res = Map.insert({FD->getCanonicalDecl(), S});
+          if (Sum.matchesAndSet(Sign, FD)) {
+            auto Res = Map.insert({FD->getCanonicalDecl(), Sum});
             assert(Res.second && "Function already has a summary set!");
             (void)Res;
             if (DisplayLoadedSummaries) {
@@ -856,44 +1006,20 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
               FD->print(llvm::errs());
               llvm::errs() << "\n";
             }
-            return;
+            return true;
           }
         }
       }
+      return false;
     }
-    // Add several summaries for the given name.
-    void operator()(StringRef Name, const std::vector<Summary> &Summaries) {
-      for (const Summary &S : Summaries)
-        operator()(Name, S);
+    // Add the same summary for different names with the Signature explicitly
+    // given.
+    void operator()(std::vector<StringRef> Names, Signature Sign, Summary Sum) {
+      for (StringRef Name : Names)
+        operator()(Name, Sign, Sum);
     }
   } addToFunctionSummaryMap(ACtx, FunctionSummaryMap, DisplayLoadedSummaries);
 
-  // We are finally ready to define specifications for all supported functions.
-  //
-  // The signature needs to have the correct number of arguments.
-  // However, we insert `Irrelevant' when the type is insignificant.
-  //
-  // Argument ranges should always cover all variants. If return value
-  // is completely unknown, omit it from the respective range set.
-  //
-  // All types in the spec need to be canonical.
-  //
-  // Every item in the list of range sets represents a particular
-  // execution path the analyzer would need to explore once
-  // the call is modeled - a new program state is constructed
-  // for every range set, and each range line in the range set
-  // corresponds to a specific constraint within this state.
-  //
-  // Upon comparing to another argument, the other argument is casted
-  // to the current argument's type. This avoids proper promotion but
-  // seems useful. For example, read() receives size_t argument,
-  // and its return value, which is of type ssize_t, cannot be greater
-  // than this argument. If we made a promotion, and the size argument
-  // is equal to, say, 10, then we'd impose a range of [0, 10] on the
-  // return value, however the correct range is [-1, 10].
-  //
-  // Please update the list of functions in the header after editing!
-
   // Below are helpers functions to create the summaries.
   auto ArgumentCondition = [](ArgNo ArgN, RangeKind Kind,
                               IntRangeVector Ranges) {
@@ -910,9 +1036,22 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
       return std::make_shared<ComparisonConstraint>(Ret, Op, OtherArgN);
     }
   } ReturnValueCondition;
-  auto Range = [](RangeInt b, RangeInt e) {
-    return IntRangeVector{std::pair<RangeInt, RangeInt>{b, e}};
-  };
+  struct {
+    auto operator()(RangeInt b, RangeInt e) {
+      return IntRangeVector{std::pair<RangeInt, RangeInt>{b, e}};
+    }
+    auto operator()(RangeInt b, Optional<RangeInt> e) {
+      if (e)
+        return IntRangeVector{std::pair<RangeInt, RangeInt>{b, *e}};
+      return IntRangeVector{};
+    }
+    auto operator()(std::pair<RangeInt, RangeInt> i0,
+                    std::pair<RangeInt, Optional<RangeInt>> i1) {
+      if (i1.second)
+        return IntRangeVector{i0, {i1.first, *(i1.second)}};
+      return IntRangeVector{i0};
+    }
+  } Range;
   auto SingleValue = [](RangeInt v) {
     return IntRangeVector{std::pair<RangeInt, RangeInt>{v, v}};
   };
@@ -921,60 +1060,28 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
     return std::make_shared<NotNullConstraint>(ArgN);
   };
 
-  Optional<QualType> FileTy = lookupType("FILE", ACtx);
-  Optional<QualType> FilePtrTy, FilePtrRestrictTy;
-  if (FileTy) {
-    // FILE *
-    FilePtrTy = ACtx.getPointerType(*FileTy);
-    // FILE *restrict
-    FilePtrRestrictTy =
-        ACtx.getLangOpts().C99 ? ACtx.getRestrictType(*FilePtrTy) : *FilePtrTy;
-  }
+  Optional<QualType> FileTy = lookupTy("FILE");
+  Optional<QualType> FilePtrTy = getPointerTy(FileTy);
+  Optional<QualType> FilePtrRestrictTy = getRestrictTy(FilePtrTy);
 
-  using RetType = QualType;
-  // Templates for summaries that are reused by many functions.
-  auto Getc = [&]() {
-    return Summary(ArgTypes{*FilePtrTy}, RetType{IntTy}, NoEvalCall)
-        .Case({ReturnValueCondition(WithinRange,
-                                    {{EOFv, EOFv}, {0, UCharRangeMax}})});
-  };
-  auto Read = [&](RetType R, RangeInt Max) {
-    return Summary(ArgTypes{Irrelevant, Irrelevant, SizeTy}, RetType{R},
-                   NoEvalCall)
-        .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-               ReturnValueCondition(WithinRange, Range(-1, Max))});
-  };
-  auto Fread = [&]() {
-    return Summary(
-               ArgTypes{VoidPtrRestrictTy, SizeTy, SizeTy, *FilePtrRestrictTy},
-               RetType{SizeTy}, NoEvalCall)
-        .Case({
-            ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-        })
-        .ArgConstraint(NotNull(ArgNo(0)));
-  };
-  auto Fwrite = [&]() {
-    return Summary(ArgTypes{ConstVoidPtrRestrictTy, SizeTy, SizeTy,
-                            *FilePtrRestrictTy},
-                   RetType{SizeTy}, NoEvalCall)
-        .Case({
-            ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-        })
-        .ArgConstraint(NotNull(ArgNo(0)));
-  };
-  auto Getline = [&](RetType R, RangeInt Max) {
-    return Summary(ArgTypes{Irrelevant, Irrelevant, Irrelevant}, RetType{R},
-                   NoEvalCall)
-        .Case({ReturnValueCondition(WithinRange, {{-1, -1}, {1, Max}})});
-  };
+  // We are finally ready to define specifications for all supported functions.
+  //
+  // Argument ranges should always cover all variants. If return value
+  // is completely unknown, omit it from the respective range set.
+  //
+  // Every item in the list of range sets represents a particular
+  // execution path the analyzer would need to explore once
+  // the call is modeled - a new program state is constructed
+  // for every range set, and each range line in the range set
+  // corresponds to a specific constraint within this state.
 
   // The isascii() family of functions.
   // The behavior is undefined if the value of the argument is not
   // representable as unsigned char or is not equal to EOF. See e.g. C99
   // 7.4.1.2 The isalpha function (p: 181-182).
   addToFunctionSummaryMap(
-      "isalnum",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isalnum", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           // Boils down to isupper() or islower() or isdigit().
           .Case({ArgumentCondition(0U, WithinRange,
                                    {{'0', '9'}, {'A', 'Z'}, {'a', 'z'}}),
@@ -991,8 +1098,8 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
           .ArgConstraint(ArgumentCondition(
               0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
   addToFunctionSummaryMap(
-      "isalpha",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isalpha", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, {{'A', 'Z'}, {'a', 'z'}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           // The locale-specific range.
@@ -1002,43 +1109,43 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
                      {{'A', 'Z'}, {'a', 'z'}, {128, UCharRangeMax}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isascii",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isascii", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range(0, 127)),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange, Range(0, 127)),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isblank",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isblank", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, {{'\t', '\t'}, {' ', ' '}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange, {{'\t', '\t'}, {' ', ' '}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "iscntrl",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "iscntrl", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, {{0, 32}, {127, 127}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange, {{0, 32}, {127, 127}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isdigit",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isdigit", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range('0', '9')),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange, Range('0', '9')),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isgraph",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isgraph", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range(33, 126)),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange, Range(33, 126)),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "islower",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "islower", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           // Is certainly lowercase.
           .Case({ArgumentCondition(0U, WithinRange, Range('a', 'z')),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
@@ -1052,15 +1159,15 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
           .Case({ArgumentCondition(0U, OutOfRange, Range(0, UCharRangeMax)),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isprint",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isprint", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range(32, 126)),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange, Range(32, 126)),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "ispunct",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "ispunct", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(
                      0U, WithinRange,
                      {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}),
@@ -1070,8 +1177,8 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
                      {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isspace",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isspace", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           // Space, '\f', '\n', '\r', '\t', '\v'.
           .Case({ArgumentCondition(0U, WithinRange, {{9, 13}, {' ', ' '}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
@@ -1081,8 +1188,8 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
                                    {{9, 13}, {' ', ' '}, {128, UCharRangeMax}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isupper",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isupper", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           // Is certainly uppercase.
           .Case({ArgumentCondition(0U, WithinRange, Range('A', 'Z')),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
@@ -1093,650 +1200,1290 @@ void StdLibraryFunctionsChecker::initFunctionSummaries(
                                    {{'A', 'Z'}, {128, UCharRangeMax}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
   addToFunctionSummaryMap(
-      "isxdigit",
-      Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+      "isxdigit", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange,
                                    {{'0', '9'}, {'A', 'F'}, {'a', 'f'}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))})
           .Case({ArgumentCondition(0U, OutOfRange,
                                    {{'0', '9'}, {'A', 'F'}, {'a', 'f'}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))}));
+  addToFunctionSummaryMap(
+      "toupper", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
+          .ArgConstraint(ArgumentCondition(
+              0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
+  addToFunctionSummaryMap(
+      "tolower", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
+          .ArgConstraint(ArgumentCondition(
+              0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
+  addToFunctionSummaryMap(
+      "toascii", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+      Summary(EvalCallAsPure)
+          .ArgConstraint(ArgumentCondition(
+              0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
 
   // The getc() family of functions that returns either a char or an EOF.
-  if (FilePtrTy) {
-    addToFunctionSummaryMap("getc", Getc());
-    addToFunctionSummaryMap("fgetc", Getc());
-  }
   addToFunctionSummaryMap(
-      "getchar", Summary(ArgTypes{}, RetType{IntTy}, NoEvalCall)
-                     .Case({ReturnValueCondition(
-                         WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})}));
+      {"getc", "fgetc"}, Signature(ArgTypes{FilePtrTy}, RetType{IntTy}),
+      Summary(NoEvalCall)
+          .Case({ReturnValueCondition(WithinRange,
+                                      {{EOFv, EOFv}, {0, UCharRangeMax}})}));
+  addToFunctionSummaryMap(
+      "getchar", Signature(ArgTypes{}, RetType{IntTy}),
+      Summary(NoEvalCall)
+          .Case({ReturnValueCondition(WithinRange,
+                                      {{EOFv, EOFv}, {0, UCharRangeMax}})}));
 
   // read()-like functions that never return more than buffer size.
-  if (FilePtrRestrictTy) {
-    addToFunctionSummaryMap("fread", Fread());
-    addToFunctionSummaryMap("fwrite", Fwrite());
-  }
+  auto FreadSummary =
+      Summary(NoEvalCall)
+          .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                 ReturnValueCondition(WithinRange, Range(0, SizeMax))})
+          .ArgConstraint(NotNull(ArgNo(0)))
+          .ArgConstraint(NotNull(ArgNo(3)))
+          .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(0), /*BufSize=*/ArgNo(1),
+                                    /*BufSizeMultiplier=*/ArgNo(2)));
+
+  // size_t fread(void *restrict ptr, size_t size, size_t nitems,
+  //              FILE *restrict stream);
+  addToFunctionSummaryMap(
+      "fread",
+      Signature(ArgTypes{VoidPtrRestrictTy, SizeTy, SizeTy, FilePtrRestrictTy},
+                RetType{SizeTy}),
+      FreadSummary);
+  // size_t fwrite(const void *restrict ptr, size_t size, size_t nitems,
+  //               FILE *restrict stream);
+  addToFunctionSummaryMap("fwrite",
+                          Signature(ArgTypes{ConstVoidPtrRestrictTy, SizeTy,
+                                             SizeTy, FilePtrRestrictTy},
+                                    RetType{SizeTy}),
+                          FreadSummary);
+
+  Optional<QualType> Ssize_tTy = lookupTy("ssize_t");
+  Optional<RangeInt> Ssize_tMax = getMaxValue(Ssize_tTy);
+
+  auto ReadSummary =
+      Summary(NoEvalCall)
+          .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                 ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))});
 
-  // We are not sure how ssize_t is defined on every platform, so we
-  // provide three variants that should cover common cases.
   // FIXME these are actually defined by POSIX and not by the C standard, we
   // should handle them together with the rest of the POSIX functions.
-  addToFunctionSummaryMap("read", {Read(IntTy, IntMax), Read(LongTy, LongMax),
-                                   Read(LongLongTy, LongLongMax)});
-  addToFunctionSummaryMap("write", {Read(IntTy, IntMax), Read(LongTy, LongMax),
-                                    Read(LongLongTy, LongLongMax)});
+  // ssize_t read(int fildes, void *buf, size_t nbyte);
+  addToFunctionSummaryMap(
+      "read", Signature(ArgTypes{IntTy, VoidPtrTy, SizeTy}, RetType{Ssize_tTy}),
+      ReadSummary);
+  // ssize_t write(int fildes, const void *buf, size_t nbyte);
+  addToFunctionSummaryMap(
+      "write",
+      Signature(ArgTypes{IntTy, ConstVoidPtrTy, SizeTy}, RetType{Ssize_tTy}),
+      ReadSummary);
+
+  auto GetLineSummary =
+      Summary(NoEvalCall)
+          .Case({ReturnValueCondition(WithinRange,
+                                      Range({-1, -1}, {1, Ssize_tMax}))});
+
+  QualType CharPtrPtrRestrictTy = getRestrictTy(getPointerTy(CharPtrTy));
 
   // getline()-like functions either fail or read at least the delimiter.
   // FIXME these are actually defined by POSIX and not by the C standard, we
   // should handle them together with the rest of the POSIX functions.
-  addToFunctionSummaryMap("getline",
-                          {Getline(IntTy, IntMax), Getline(LongTy, LongMax),
-                           Getline(LongLongTy, LongLongMax)});
-  addToFunctionSummaryMap("getdelim",
-                          {Getline(IntTy, IntMax), Getline(LongTy, LongMax),
-                           Getline(LongLongTy, LongLongMax)});
+  // ssize_t getline(char **restrict lineptr, size_t *restrict n,
+  //                 FILE *restrict stream);
+  addToFunctionSummaryMap(
+      "getline",
+      Signature(
+          ArgTypes{CharPtrPtrRestrictTy, SizePtrRestrictTy, FilePtrRestrictTy},
+          RetType{Ssize_tTy}),
+      GetLineSummary);
+  // ssize_t getdelim(char **restrict lineptr, size_t *restrict n,
+  //                  int delimiter, FILE *restrict stream);
+  addToFunctionSummaryMap(
+      "getdelim",
+      Signature(ArgTypes{CharPtrPtrRestrictTy, SizePtrRestrictTy, IntTy,
+                         FilePtrRestrictTy},
+                RetType{Ssize_tTy}),
+      GetLineSummary);
 
   if (ModelPOSIX) {
 
     // long a64l(const char *str64);
     addToFunctionSummaryMap(
-        "a64l", Summary(ArgTypes{ConstCharPtrTy}, RetType{LongTy}, NoEvalCall)
-                    .ArgConstraint(NotNull(ArgNo(0))));
+        "a64l", Signature(ArgTypes{ConstCharPtrTy}, RetType{LongTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // char *l64a(long value);
-    addToFunctionSummaryMap(
-        "l64a", Summary(ArgTypes{LongTy}, RetType{CharPtrTy}, NoEvalCall)
-                    .ArgConstraint(
-                        ArgumentCondition(0, WithinRange, Range(0, LongMax))));
+    addToFunctionSummaryMap("l64a",
+                            Signature(ArgTypes{LongTy}, RetType{CharPtrTy}),
+                            Summary(NoEvalCall)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, LongMax))));
+
+    const auto ReturnsZeroOrMinusOne =
+        ConstraintSet{ReturnValueCondition(WithinRange, Range(-1, 0))};
+    const auto ReturnsFileDescriptor =
+        ConstraintSet{ReturnValueCondition(WithinRange, Range(-1, IntMax))};
 
     // int access(const char *pathname, int amode);
-    addToFunctionSummaryMap("access", Summary(ArgTypes{ConstCharPtrTy, IntTy},
-                                              RetType{IntTy}, NoEvalCall)
-                                          .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap(
+        "access", Signature(ArgTypes{ConstCharPtrTy, IntTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
     // int faccessat(int dirfd, const char *pathname, int mode, int flags);
     addToFunctionSummaryMap(
-        "faccessat", Summary(ArgTypes{IntTy, ConstCharPtrTy, IntTy, IntTy},
-                             RetType{IntTy}, NoEvalCall)
-                         .ArgConstraint(NotNull(ArgNo(1))));
+        "faccessat",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, IntTy, IntTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(1))));
 
     // int dup(int fildes);
-    addToFunctionSummaryMap(
-        "dup", Summary(ArgTypes{IntTy}, RetType{IntTy}, NoEvalCall)
-                   .ArgConstraint(
-                       ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+    addToFunctionSummaryMap("dup", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsFileDescriptor)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, IntMax))));
 
     // int dup2(int fildes1, int filedes2);
     addToFunctionSummaryMap(
-        "dup2",
-        Summary(ArgTypes{IntTy, IntTy}, RetType{IntTy}, NoEvalCall)
+        "dup2", Signature(ArgTypes{IntTy, IntTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsFileDescriptor)
             .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
             .ArgConstraint(
                 ArgumentCondition(1, WithinRange, Range(0, IntMax))));
 
     // int fdatasync(int fildes);
-    addToFunctionSummaryMap(
-        "fdatasync", Summary(ArgTypes{IntTy}, RetType{IntTy}, NoEvalCall)
-                         .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                          Range(0, IntMax))));
+    addToFunctionSummaryMap("fdatasync",
+                            Signature(ArgTypes{IntTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, IntMax))));
 
     // int fnmatch(const char *pattern, const char *string, int flags);
     addToFunctionSummaryMap(
-        "fnmatch", Summary(ArgTypes{ConstCharPtrTy, ConstCharPtrTy, IntTy},
-                           RetType{IntTy}, EvalCallAsPure)
-                       .ArgConstraint(NotNull(ArgNo(0)))
-                       .ArgConstraint(NotNull(ArgNo(1))));
+        "fnmatch",
+        Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy, IntTy},
+                  RetType{IntTy}),
+        Summary(EvalCallAsPure)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
     // int fsync(int fildes);
-    addToFunctionSummaryMap(
-        "fsync", Summary(ArgTypes{IntTy}, RetType{IntTy}, NoEvalCall)
-                     .ArgConstraint(
-                         ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+    addToFunctionSummaryMap("fsync", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, IntMax))));
 
-    Optional<QualType> Off_tTy = lookupType("off_t", ACtx);
+    Optional<QualType> Off_tTy = lookupTy("off_t");
 
-    if (Off_tTy)
-      // int truncate(const char *path, off_t length);
-      addToFunctionSummaryMap("truncate",
-                              Summary(ArgTypes{ConstCharPtrTy, *Off_tTy},
-                                      RetType{IntTy}, NoEvalCall)
-                                  .ArgConstraint(NotNull(ArgNo(0))));
+    // int truncate(const char *path, off_t length);
+    addToFunctionSummaryMap(
+        "truncate",
+        Signature(ArgTypes{ConstCharPtrTy, Off_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
     // int symlink(const char *oldpath, const char *newpath);
-    addToFunctionSummaryMap("symlink",
-                            Summary(ArgTypes{ConstCharPtrTy, ConstCharPtrTy},
-                                    RetType{IntTy}, NoEvalCall)
-                                .ArgConstraint(NotNull(ArgNo(0)))
-                                .ArgConstraint(NotNull(ArgNo(1))));
+    addToFunctionSummaryMap(
+        "symlink",
+        Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
     // int symlinkat(const char *oldpath, int newdirfd, const char *newpath);
     addToFunctionSummaryMap(
         "symlinkat",
-        Summary(ArgTypes{ConstCharPtrTy, IntTy, ConstCharPtrTy}, RetType{IntTy},
-                NoEvalCall)
+        Signature(ArgTypes{ConstCharPtrTy, IntTy, ConstCharPtrTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
             .ArgConstraint(NotNull(ArgNo(0)))
             .ArgConstraint(ArgumentCondition(1, WithinRange, Range(0, IntMax)))
             .ArgConstraint(NotNull(ArgNo(2))));
 
-    if (Off_tTy)
-      // int lockf(int fd, int cmd, off_t len);
-      addToFunctionSummaryMap(
-          "lockf",
-          Summary(ArgTypes{IntTy, IntTy, *Off_tTy}, RetType{IntTy}, NoEvalCall)
-              .ArgConstraint(
-                  ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+    // int lockf(int fd, int cmd, off_t len);
+    addToFunctionSummaryMap(
+        "lockf", Signature(ArgTypes{IntTy, IntTy, Off_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-    Optional<QualType> Mode_tTy = lookupType("mode_t", ACtx);
+    Optional<QualType> Mode_tTy = lookupTy("mode_t");
 
-    if (Mode_tTy)
-      // int creat(const char *pathname, mode_t mode);
-      addToFunctionSummaryMap("creat",
-                              Summary(ArgTypes{ConstCharPtrTy, *Mode_tTy},
-                                      RetType{IntTy}, NoEvalCall)
-                                  .ArgConstraint(NotNull(ArgNo(0))));
+    // int creat(const char *pathname, mode_t mode);
+    addToFunctionSummaryMap(
+        "creat", Signature(ArgTypes{ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsFileDescriptor)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
     // unsigned int sleep(unsigned int seconds);
     addToFunctionSummaryMap(
-        "sleep",
-        Summary(ArgTypes{UnsignedIntTy}, RetType{UnsignedIntTy}, NoEvalCall)
+        "sleep", Signature(ArgTypes{UnsignedIntTy}, RetType{UnsignedIntTy}),
+        Summary(NoEvalCall)
             .ArgConstraint(
                 ArgumentCondition(0, WithinRange, Range(0, UnsignedIntMax))));
 
-    Optional<QualType> DirTy = lookupType("DIR", ACtx);
-    Optional<QualType> DirPtrTy;
-    if (DirTy)
-      DirPtrTy = ACtx.getPointerType(*DirTy);
+    Optional<QualType> DirTy = lookupTy("DIR");
+    Optional<QualType> DirPtrTy = getPointerTy(DirTy);
 
-    if (DirPtrTy)
-      // int dirfd(DIR *dirp);
-      addToFunctionSummaryMap(
-          "dirfd", Summary(ArgTypes{*DirPtrTy}, RetType{IntTy}, NoEvalCall)
-                       .ArgConstraint(NotNull(ArgNo(0))));
+    // int dirfd(DIR *dirp);
+    addToFunctionSummaryMap("dirfd",
+                            Signature(ArgTypes{DirPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsFileDescriptor)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
     // unsigned int alarm(unsigned int seconds);
     addToFunctionSummaryMap(
-        "alarm",
-        Summary(ArgTypes{UnsignedIntTy}, RetType{UnsignedIntTy}, NoEvalCall)
+        "alarm", Signature(ArgTypes{UnsignedIntTy}, RetType{UnsignedIntTy}),
+        Summary(NoEvalCall)
             .ArgConstraint(
                 ArgumentCondition(0, WithinRange, Range(0, UnsignedIntMax))));
 
-    if (DirPtrTy)
-      // int closedir(DIR *dir);
-      addToFunctionSummaryMap(
-          "closedir", Summary(ArgTypes{*DirPtrTy}, RetType{IntTy}, NoEvalCall)
-                          .ArgConstraint(NotNull(ArgNo(0))));
+    // int closedir(DIR *dir);
+    addToFunctionSummaryMap("closedir",
+                            Signature(ArgTypes{DirPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
     // char *strdup(const char *s);
-    addToFunctionSummaryMap("strdup", Summary(ArgTypes{ConstCharPtrTy},
-                                              RetType{CharPtrTy}, NoEvalCall)
-                                          .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap(
+        "strdup", Signature(ArgTypes{ConstCharPtrTy}, RetType{CharPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // char *strndup(const char *s, size_t n);
     addToFunctionSummaryMap(
-        "strndup", Summary(ArgTypes{ConstCharPtrTy, SizeTy}, RetType{CharPtrTy},
-                           NoEvalCall)
-                       .ArgConstraint(NotNull(ArgNo(0)))
-                       .ArgConstraint(ArgumentCondition(1, WithinRange,
-                                                        Range(0, SizeMax))));
+        "strndup",
+        Signature(ArgTypes{ConstCharPtrTy, SizeTy}, RetType{CharPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(
+                ArgumentCondition(1, WithinRange, Range(0, SizeMax))));
 
     // wchar_t *wcsdup(const wchar_t *s);
-    addToFunctionSummaryMap("wcsdup", Summary(ArgTypes{ConstWchar_tPtrTy},
-                                              RetType{Wchar_tPtrTy}, NoEvalCall)
-                                          .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap(
+        "wcsdup", Signature(ArgTypes{ConstWchar_tPtrTy}, RetType{Wchar_tPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // int mkstemp(char *template);
-    addToFunctionSummaryMap(
-        "mkstemp", Summary(ArgTypes{CharPtrTy}, RetType{IntTy}, NoEvalCall)
-                       .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap("mkstemp",
+                            Signature(ArgTypes{CharPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsFileDescriptor)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
     // char *mkdtemp(char *template);
     addToFunctionSummaryMap(
-        "mkdtemp", Summary(ArgTypes{CharPtrTy}, RetType{CharPtrTy}, NoEvalCall)
-                       .ArgConstraint(NotNull(ArgNo(0))));
+        "mkdtemp", Signature(ArgTypes{CharPtrTy}, RetType{CharPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // char *getcwd(char *buf, size_t size);
     addToFunctionSummaryMap(
-        "getcwd",
-        Summary(ArgTypes{CharPtrTy, SizeTy}, RetType{CharPtrTy}, NoEvalCall)
+        "getcwd", Signature(ArgTypes{CharPtrTy, SizeTy}, RetType{CharPtrTy}),
+        Summary(NoEvalCall)
             .ArgConstraint(
                 ArgumentCondition(1, WithinRange, Range(0, SizeMax))));
 
-    if (Mode_tTy) {
-      // int mkdir(const char *pathname, mode_t mode);
-      addToFunctionSummaryMap("mkdir",
-                              Summary(ArgTypes{ConstCharPtrTy, *Mode_tTy},
-                                      RetType{IntTy}, NoEvalCall)
-                                  .ArgConstraint(NotNull(ArgNo(0))));
+    // int mkdir(const char *pathname, mode_t mode);
+    addToFunctionSummaryMap(
+        "mkdir", Signature(ArgTypes{ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-      // int mkdirat(int dirfd, const char *pathname, mode_t mode);
-      addToFunctionSummaryMap(
-          "mkdirat", Summary(ArgTypes{IntTy, ConstCharPtrTy, *Mode_tTy},
-                             RetType{IntTy}, NoEvalCall)
-                         .ArgConstraint(NotNull(ArgNo(1))));
-    }
+    // int mkdirat(int dirfd, const char *pathname, mode_t mode);
+    addToFunctionSummaryMap(
+        "mkdirat",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-    Optional<QualType> Dev_tTy = lookupType("dev_t", ACtx);
+    Optional<QualType> Dev_tTy = lookupTy("dev_t");
 
-    if (Mode_tTy && Dev_tTy) {
-      // int mknod(const char *pathname, mode_t mode, dev_t dev);
-      addToFunctionSummaryMap(
-          "mknod", Summary(ArgTypes{ConstCharPtrTy, *Mode_tTy, *Dev_tTy},
-                           RetType{IntTy}, NoEvalCall)
-                       .ArgConstraint(NotNull(ArgNo(0))));
-
-      // int mknodat(int dirfd, const char *pathname, mode_t mode, dev_t dev);
-      addToFunctionSummaryMap("mknodat", Summary(ArgTypes{IntTy, ConstCharPtrTy,
-                                                          *Mode_tTy, *Dev_tTy},
-                                                 RetType{IntTy}, NoEvalCall)
-                                             .ArgConstraint(NotNull(ArgNo(1))));
-    }
+    // int mknod(const char *pathname, mode_t mode, dev_t dev);
+    addToFunctionSummaryMap(
+        "mknod",
+        Signature(ArgTypes{ConstCharPtrTy, Mode_tTy, Dev_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-    if (Mode_tTy) {
-      // int chmod(const char *path, mode_t mode);
-      addToFunctionSummaryMap("chmod",
-                              Summary(ArgTypes{ConstCharPtrTy, *Mode_tTy},
-                                      RetType{IntTy}, NoEvalCall)
-                                  .ArgConstraint(NotNull(ArgNo(0))));
+    // int mknodat(int dirfd, const char *pathname, mode_t mode, dev_t dev);
+    addToFunctionSummaryMap(
+        "mknodat",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, Mode_tTy, Dev_tTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-      // int fchmodat(int dirfd, const char *pathname, mode_t mode, int flags);
-      addToFunctionSummaryMap(
-          "fchmodat", Summary(ArgTypes{IntTy, ConstCharPtrTy, *Mode_tTy, IntTy},
-                              RetType{IntTy}, NoEvalCall)
-                          .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                           Range(0, IntMax)))
-                          .ArgConstraint(NotNull(ArgNo(1))));
+    // int chmod(const char *path, mode_t mode);
+    addToFunctionSummaryMap(
+        "chmod", Signature(ArgTypes{ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-      // int fchmod(int fildes, mode_t mode);
-      addToFunctionSummaryMap(
-          "fchmod",
-          Summary(ArgTypes{IntTy, *Mode_tTy}, RetType{IntTy}, NoEvalCall)
-              .ArgConstraint(
-                  ArgumentCondition(0, WithinRange, Range(0, IntMax))));
-    }
+    // int fchmodat(int dirfd, const char *pathname, mode_t mode, int flags);
+    addToFunctionSummaryMap(
+        "fchmodat",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, Mode_tTy, IntTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-    Optional<QualType> Uid_tTy = lookupType("uid_t", ACtx);
-    Optional<QualType> Gid_tTy = lookupType("gid_t", ACtx);
+    // int fchmod(int fildes, mode_t mode);
+    addToFunctionSummaryMap(
+        "fchmod", Signature(ArgTypes{IntTy, Mode_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-    if (Uid_tTy && Gid_tTy) {
-      // int fchownat(int dirfd, const char *pathname, uid_t owner, gid_t group,
-      //              int flags);
-      addToFunctionSummaryMap(
-          "fchownat",
-          Summary(ArgTypes{IntTy, ConstCharPtrTy, *Uid_tTy, *Gid_tTy, IntTy},
-                  RetType{IntTy}, NoEvalCall)
-              .ArgConstraint(
-                  ArgumentCondition(0, WithinRange, Range(0, IntMax)))
-              .ArgConstraint(NotNull(ArgNo(1))));
+    Optional<QualType> Uid_tTy = lookupTy("uid_t");
+    Optional<QualType> Gid_tTy = lookupTy("gid_t");
 
-      // int chown(const char *path, uid_t owner, gid_t group);
-      addToFunctionSummaryMap(
-          "chown", Summary(ArgTypes{ConstCharPtrTy, *Uid_tTy, *Gid_tTy},
-                           RetType{IntTy}, NoEvalCall)
-                       .ArgConstraint(NotNull(ArgNo(0))));
+    // int fchownat(int dirfd, const char *pathname, uid_t owner, gid_t group,
+    //              int flags);
+    addToFunctionSummaryMap(
+        "fchownat",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, Uid_tTy, Gid_tTy, IntTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-      // int lchown(const char *path, uid_t owner, gid_t group);
-      addToFunctionSummaryMap(
-          "lchown", Summary(ArgTypes{ConstCharPtrTy, *Uid_tTy, *Gid_tTy},
-                            RetType{IntTy}, NoEvalCall)
-                        .ArgConstraint(NotNull(ArgNo(0))));
+    // int chown(const char *path, uid_t owner, gid_t group);
+    addToFunctionSummaryMap(
+        "chown",
+        Signature(ArgTypes{ConstCharPtrTy, Uid_tTy, Gid_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-      // int fchown(int fildes, uid_t owner, gid_t group);
-      addToFunctionSummaryMap(
-          "fchown", Summary(ArgTypes{IntTy, *Uid_tTy, *Gid_tTy}, RetType{IntTy},
-                            NoEvalCall)
-                        .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                         Range(0, IntMax))));
-    }
+    // int lchown(const char *path, uid_t owner, gid_t group);
+    addToFunctionSummaryMap(
+        "lchown",
+        Signature(ArgTypes{ConstCharPtrTy, Uid_tTy, Gid_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-    // int rmdir(const char *pathname);
+    // int fchown(int fildes, uid_t owner, gid_t group);
     addToFunctionSummaryMap(
-        "rmdir", Summary(ArgTypes{ConstCharPtrTy}, RetType{IntTy}, NoEvalCall)
-                     .ArgConstraint(NotNull(ArgNo(0))));
+        "fchown", Signature(ArgTypes{IntTy, Uid_tTy, Gid_tTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+
+    // int rmdir(const char *pathname);
+    addToFunctionSummaryMap("rmdir",
+                            Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
     // int chdir(const char *path);
-    addToFunctionSummaryMap(
-        "chdir", Summary(ArgTypes{ConstCharPtrTy}, RetType{IntTy}, NoEvalCall)
-                     .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap("chdir",
+                            Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
     // int link(const char *oldpath, const char *newpath);
-    addToFunctionSummaryMap("link",
-                            Summary(ArgTypes{ConstCharPtrTy, ConstCharPtrTy},
-                                    RetType{IntTy}, NoEvalCall)
-                                .ArgConstraint(NotNull(ArgNo(0)))
-                                .ArgConstraint(NotNull(ArgNo(1))));
+    addToFunctionSummaryMap(
+        "link",
+        Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
     // int linkat(int fd1, const char *path1, int fd2, const char *path2,
     //            int flag);
     addToFunctionSummaryMap(
         "linkat",
-        Summary(ArgTypes{IntTy, ConstCharPtrTy, IntTy, ConstCharPtrTy, IntTy},
-                RetType{IntTy}, NoEvalCall)
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, IntTy, ConstCharPtrTy, IntTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
             .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
             .ArgConstraint(NotNull(ArgNo(1)))
             .ArgConstraint(ArgumentCondition(2, WithinRange, Range(0, IntMax)))
             .ArgConstraint(NotNull(ArgNo(3))));
 
     // int unlink(const char *pathname);
-    addToFunctionSummaryMap(
-        "unlink", Summary(ArgTypes{ConstCharPtrTy}, RetType{IntTy}, NoEvalCall)
-                      .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap("unlink",
+                            Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
     // int unlinkat(int fd, const char *path, int flag);
     addToFunctionSummaryMap(
         "unlinkat",
-        Summary(ArgTypes{IntTy, ConstCharPtrTy, IntTy}, RetType{IntTy},
-                NoEvalCall)
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, IntTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
             .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
             .ArgConstraint(NotNull(ArgNo(1))));
 
-    Optional<QualType> StructStatTy = lookupType("stat", ACtx);
-    Optional<QualType> StructStatPtrTy, StructStatPtrRestrictTy;
-    if (StructStatTy) {
-      StructStatPtrTy = ACtx.getPointerType(*StructStatTy);
-      StructStatPtrRestrictTy = ACtx.getLangOpts().C99
-                                    ? ACtx.getRestrictType(*StructStatPtrTy)
-                                    : *StructStatPtrTy;
-    }
+    Optional<QualType> StructStatTy = lookupTy("stat");
+    Optional<QualType> StructStatPtrTy = getPointerTy(StructStatTy);
+    Optional<QualType> StructStatPtrRestrictTy = getRestrictTy(StructStatPtrTy);
 
-    if (StructStatPtrTy)
-      // int fstat(int fd, struct stat *statbuf);
-      addToFunctionSummaryMap(
-          "fstat",
-          Summary(ArgTypes{IntTy, *StructStatPtrTy}, RetType{IntTy}, NoEvalCall)
-              .ArgConstraint(
-                  ArgumentCondition(0, WithinRange, Range(0, IntMax)))
-              .ArgConstraint(NotNull(ArgNo(1))));
+    // int fstat(int fd, struct stat *statbuf);
+    addToFunctionSummaryMap(
+        "fstat", Signature(ArgTypes{IntTy, StructStatPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-    if (StructStatPtrRestrictTy) {
-      // int stat(const char *restrict path, struct stat *restrict buf);
-      addToFunctionSummaryMap(
-          "stat",
-          Summary(ArgTypes{ConstCharPtrRestrictTy, *StructStatPtrRestrictTy},
-                  RetType{IntTy}, NoEvalCall)
-              .ArgConstraint(NotNull(ArgNo(0)))
-              .ArgConstraint(NotNull(ArgNo(1))));
+    // int stat(const char *restrict path, struct stat *restrict buf);
+    addToFunctionSummaryMap(
+        "stat",
+        Signature(ArgTypes{ConstCharPtrRestrictTy, StructStatPtrRestrictTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-      // int lstat(const char *restrict path, struct stat *restrict buf);
-      addToFunctionSummaryMap(
-          "lstat",
-          Summary(ArgTypes{ConstCharPtrRestrictTy, *StructStatPtrRestrictTy},
-                  RetType{IntTy}, NoEvalCall)
-              .ArgConstraint(NotNull(ArgNo(0)))
-              .ArgConstraint(NotNull(ArgNo(1))));
-
-      // int fstatat(int fd, const char *restrict path,
-      //             struct stat *restrict buf, int flag);
-      addToFunctionSummaryMap(
-          "fstatat", Summary(ArgTypes{IntTy, ConstCharPtrRestrictTy,
-                                      *StructStatPtrRestrictTy, IntTy},
-                             RetType{IntTy}, NoEvalCall)
-                         .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                          Range(0, IntMax)))
-                         .ArgConstraint(NotNull(ArgNo(1)))
-                         .ArgConstraint(NotNull(ArgNo(2))));
-    }
+    // int lstat(const char *restrict path, struct stat *restrict buf);
+    addToFunctionSummaryMap(
+        "lstat",
+        Signature(ArgTypes{ConstCharPtrRestrictTy, StructStatPtrRestrictTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-    if (DirPtrTy) {
-      // DIR *opendir(const char *name);
-      addToFunctionSummaryMap("opendir", Summary(ArgTypes{ConstCharPtrTy},
-                                                 RetType{*DirPtrTy}, NoEvalCall)
-                                             .ArgConstraint(NotNull(ArgNo(0))));
+    // int fstatat(int fd, const char *restrict path,
+    //             struct stat *restrict buf, int flag);
+    addToFunctionSummaryMap(
+        "fstatat",
+        Signature(ArgTypes{IntTy, ConstCharPtrRestrictTy,
+                           StructStatPtrRestrictTy, IntTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(NotNull(ArgNo(2))));
 
-      // DIR *fdopendir(int fd);
-      addToFunctionSummaryMap(
-          "fdopendir", Summary(ArgTypes{IntTy}, RetType{*DirPtrTy}, NoEvalCall)
-                           .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                            Range(0, IntMax))));
-    }
+    // DIR *opendir(const char *name);
+    addToFunctionSummaryMap(
+        "opendir", Signature(ArgTypes{ConstCharPtrTy}, RetType{DirPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // DIR *fdopendir(int fd);
+    addToFunctionSummaryMap("fdopendir",
+                            Signature(ArgTypes{IntTy}, RetType{DirPtrTy}),
+                            Summary(NoEvalCall)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, IntMax))));
 
     // int isatty(int fildes);
     addToFunctionSummaryMap(
-        "isatty", Summary(ArgTypes{IntTy}, RetType{IntTy}, NoEvalCall)
-                      .ArgConstraint(
-                          ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+        "isatty", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(WithinRange, Range(0, 1))})
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-    if (FilePtrTy) {
-      // FILE *popen(const char *command, const char *type);
-      addToFunctionSummaryMap("popen",
-                              Summary(ArgTypes{ConstCharPtrTy, ConstCharPtrTy},
-                                      RetType{*FilePtrTy}, NoEvalCall)
-                                  .ArgConstraint(NotNull(ArgNo(0)))
-                                  .ArgConstraint(NotNull(ArgNo(1))));
+    // FILE *popen(const char *command, const char *type);
+    addToFunctionSummaryMap(
+        "popen",
+        Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy}, RetType{FilePtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-      // int pclose(FILE *stream);
-      addToFunctionSummaryMap(
-          "pclose", Summary(ArgTypes{*FilePtrTy}, RetType{IntTy}, NoEvalCall)
-                        .ArgConstraint(NotNull(ArgNo(0))));
-    }
+    // int pclose(FILE *stream);
+    addToFunctionSummaryMap(
+        "pclose", Signature(ArgTypes{FilePtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // int close(int fildes);
-    addToFunctionSummaryMap(
-        "close", Summary(ArgTypes{IntTy}, RetType{IntTy}, NoEvalCall)
-                     .ArgConstraint(
-                         ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+    addToFunctionSummaryMap("close", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(-1, IntMax))));
 
     // long fpathconf(int fildes, int name);
-    addToFunctionSummaryMap(
-        "fpathconf",
-        Summary(ArgTypes{IntTy, IntTy}, RetType{LongTy}, NoEvalCall)
-            .ArgConstraint(
-                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+    addToFunctionSummaryMap("fpathconf",
+                            Signature(ArgTypes{IntTy, IntTy}, RetType{LongTy}),
+                            Summary(NoEvalCall)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, IntMax))));
 
     // long pathconf(const char *path, int name);
-    addToFunctionSummaryMap("pathconf", Summary(ArgTypes{ConstCharPtrTy, IntTy},
-                                                RetType{LongTy}, NoEvalCall)
-                                            .ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap(
+        "pathconf", Signature(ArgTypes{ConstCharPtrTy, IntTy}, RetType{LongTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
-    if (FilePtrTy)
-      // FILE *fdopen(int fd, const char *mode);
-      addToFunctionSummaryMap(
-          "fdopen", Summary(ArgTypes{IntTy, ConstCharPtrTy},
-                            RetType{*FilePtrTy}, NoEvalCall)
-                        .ArgConstraint(
-                            ArgumentCondition(0, WithinRange, Range(0, IntMax)))
-                        .ArgConstraint(NotNull(ArgNo(1))));
-
-    if (DirPtrTy) {
-      // void rewinddir(DIR *dir);
-      addToFunctionSummaryMap(
-          "rewinddir", Summary(ArgTypes{*DirPtrTy}, RetType{VoidTy}, NoEvalCall)
-                           .ArgConstraint(NotNull(ArgNo(0))));
+    // FILE *fdopen(int fd, const char *mode);
+    addToFunctionSummaryMap(
+        "fdopen",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy}, RetType{FilePtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1))));
 
-      // void seekdir(DIR *dirp, long loc);
-      addToFunctionSummaryMap("seekdir", Summary(ArgTypes{*DirPtrTy, LongTy},
-                                                 RetType{VoidTy}, NoEvalCall)
-                                             .ArgConstraint(NotNull(ArgNo(0))));
-    }
+    // void rewinddir(DIR *dir);
+    addToFunctionSummaryMap(
+        "rewinddir", Signature(ArgTypes{DirPtrTy}, RetType{VoidTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // void seekdir(DIR *dirp, long loc);
+    addToFunctionSummaryMap(
+        "seekdir", Signature(ArgTypes{DirPtrTy, LongTy}, RetType{VoidTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // int rand_r(unsigned int *seedp);
-    addToFunctionSummaryMap("rand_r", Summary(ArgTypes{UnsignedIntPtrTy},
-                                              RetType{IntTy}, NoEvalCall)
-                                          .ArgConstraint(NotNull(ArgNo(0))));
-
-    // int strcasecmp(const char *s1, const char *s2);
-    addToFunctionSummaryMap("strcasecmp",
-                            Summary(ArgTypes{ConstCharPtrTy, ConstCharPtrTy},
-                                    RetType{IntTy}, EvalCallAsPure)
-                                .ArgConstraint(NotNull(ArgNo(0)))
-                                .ArgConstraint(NotNull(ArgNo(1))));
+    addToFunctionSummaryMap(
+        "rand_r", Signature(ArgTypes{UnsignedIntPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // int fileno(FILE *stream);
+    addToFunctionSummaryMap("fileno",
+                            Signature(ArgTypes{FilePtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsFileDescriptor)
+                                .ArgConstraint(NotNull(ArgNo(0))));
 
-    // int strncasecmp(const char *s1, const char *s2, size_t n);
+    // int fseeko(FILE *stream, off_t offset, int whence);
     addToFunctionSummaryMap(
-        "strncasecmp", Summary(ArgTypes{ConstCharPtrTy, ConstCharPtrTy, SizeTy},
-                               RetType{IntTy}, EvalCallAsPure)
-                           .ArgConstraint(NotNull(ArgNo(0)))
-                           .ArgConstraint(NotNull(ArgNo(1)))
-                           .ArgConstraint(ArgumentCondition(
-                               2, WithinRange, Range(0, SizeMax))));
+        "fseeko",
+        Signature(ArgTypes{FilePtrTy, Off_tTy, IntTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-    if (FilePtrTy && Off_tTy) {
+    // off_t ftello(FILE *stream);
+    addToFunctionSummaryMap(
+        "ftello", Signature(ArgTypes{FilePtrTy}, RetType{Off_tTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
-      // int fileno(FILE *stream);
-      addToFunctionSummaryMap(
-          "fileno", Summary(ArgTypes{*FilePtrTy}, RetType{IntTy}, NoEvalCall)
-                        .ArgConstraint(NotNull(ArgNo(0))));
+    // void *mmap(void *addr, size_t length, int prot, int flags, int fd,
+    // off_t offset);
+    addToFunctionSummaryMap(
+        "mmap",
+        Signature(ArgTypes{VoidPtrTy, SizeTy, IntTy, IntTy, IntTy, Off_tTy},
+                  RetType{VoidPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(ArgumentCondition(1, WithinRange, Range(1, SizeMax)))
+            .ArgConstraint(
+                ArgumentCondition(4, WithinRange, Range(-1, IntMax))));
 
-      // int fseeko(FILE *stream, off_t offset, int whence);
-      addToFunctionSummaryMap("fseeko",
-                              Summary(ArgTypes{*FilePtrTy, *Off_tTy, IntTy},
-                                      RetType{IntTy}, NoEvalCall)
-                                  .ArgConstraint(NotNull(ArgNo(0))));
+    Optional<QualType> Off64_tTy = lookupTy("off64_t");
+    // void *mmap64(void *addr, size_t length, int prot, int flags, int fd,
+    // off64_t offset);
+    addToFunctionSummaryMap(
+        "mmap64",
+        Signature(ArgTypes{VoidPtrTy, SizeTy, IntTy, IntTy, IntTy, Off64_tTy},
+                  RetType{VoidPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(ArgumentCondition(1, WithinRange, Range(1, SizeMax)))
+            .ArgConstraint(
+                ArgumentCondition(4, WithinRange, Range(-1, IntMax))));
 
-      // off_t ftello(FILE *stream);
-      addToFunctionSummaryMap(
-          "ftello", Summary(ArgTypes{*FilePtrTy}, RetType{*Off_tTy}, NoEvalCall)
-                        .ArgConstraint(NotNull(ArgNo(0))));
-    }
+    // int pipe(int fildes[2]);
+    addToFunctionSummaryMap("pipe",
+                            Signature(ArgTypes{IntPtrTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(NotNull(ArgNo(0))));
+
+    // off_t lseek(int fildes, off_t offset, int whence);
+    addToFunctionSummaryMap(
+        "lseek", Signature(ArgTypes{IntTy, Off_tTy, IntTy}, RetType{Off_tTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+
+    // ssize_t readlink(const char *restrict path, char *restrict buf,
+    //                  size_t bufsize);
+    addToFunctionSummaryMap(
+        "readlink",
+        Signature(ArgTypes{ConstCharPtrRestrictTy, CharPtrRestrictTy, SizeTy},
+                  RetType{Ssize_tTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
+                                      /*BufSize=*/ArgNo(2)))
+            .ArgConstraint(
+                ArgumentCondition(2, WithinRange, Range(0, SizeMax))));
+
+    // ssize_t readlinkat(int fd, const char *restrict path,
+    //                    char *restrict buf, size_t bufsize);
+    addToFunctionSummaryMap(
+        "readlinkat",
+        Signature(
+            ArgTypes{IntTy, ConstCharPtrRestrictTy, CharPtrRestrictTy, SizeTy},
+            RetType{Ssize_tTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(LessThanOrEq, ArgNo(3)),
+                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(NotNull(ArgNo(2)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(2),
+                                      /*BufSize=*/ArgNo(3)))
+            .ArgConstraint(
+                ArgumentCondition(3, WithinRange, Range(0, SizeMax))));
+
+    // int renameat(int olddirfd, const char *oldpath, int newdirfd, const char
+    // *newpath);
+    addToFunctionSummaryMap(
+        "renameat",
+        Signature(ArgTypes{IntTy, ConstCharPtrTy, IntTy, ConstCharPtrTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(NotNull(ArgNo(3))));
+
+    // char *realpath(const char *restrict file_name,
+    //                char *restrict resolved_name);
+    addToFunctionSummaryMap(
+        "realpath",
+        Signature(ArgTypes{ConstCharPtrRestrictTy, CharPtrRestrictTy},
+                  RetType{CharPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    QualType CharPtrConstPtr = getPointerTy(getConstTy(CharPtrTy));
+
+    // int execv(const char *path, char *const argv[]);
+    addToFunctionSummaryMap(
+        "execv",
+        Signature(ArgTypes{ConstCharPtrTy, CharPtrConstPtr}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(WithinRange, SingleValue(-1))})
+            .ArgConstraint(NotNull(ArgNo(0))));
+
+    // int execvp(const char *file, char *const argv[]);
+    addToFunctionSummaryMap(
+        "execvp",
+        Signature(ArgTypes{ConstCharPtrTy, CharPtrConstPtr}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(WithinRange, SingleValue(-1))})
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-    if (Off_tTy) {
-      Optional<RangeInt> Off_tMax = BVF.getMaxValue(*Off_tTy).getLimitedValue();
+    // int getopt(int argc, char * const argv[], const char *optstring);
+    addToFunctionSummaryMap(
+        "getopt",
+        Signature(ArgTypes{IntTy, CharPtrConstPtr, ConstCharPtrTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(WithinRange, Range(-1, UCharRangeMax))})
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(NotNull(ArgNo(2))));
 
-      // void *mmap(void *addr, size_t length, int prot, int flags, int fd,
-      // off_t offset);
+    Optional<QualType> StructSockaddrTy = lookupTy("sockaddr");
+    Optional<QualType> StructSockaddrPtrTy = getPointerTy(StructSockaddrTy);
+    Optional<QualType> ConstStructSockaddrPtrTy =
+        getPointerTy(getConstTy(StructSockaddrTy));
+    Optional<QualType> StructSockaddrPtrRestrictTy =
+        getRestrictTy(StructSockaddrPtrTy);
+    Optional<QualType> ConstStructSockaddrPtrRestrictTy =
+        getRestrictTy(ConstStructSockaddrPtrTy);
+    Optional<QualType> Socklen_tTy = lookupTy("socklen_t");
+    Optional<QualType> Socklen_tPtrTy = getPointerTy(Socklen_tTy);
+    Optional<QualType> Socklen_tPtrRestrictTy = getRestrictTy(Socklen_tPtrTy);
+    Optional<RangeInt> Socklen_tMax = getMaxValue(Socklen_tTy);
+
+    // In 'socket.h' of some libc implementations with C99, sockaddr parameter
+    // is a transparent union of the underlying sockaddr_ family of pointers
+    // instead of being a pointer to struct sockaddr. In these cases, the
+    // standardized signature will not match, thus we try to match with another
+    // signature that has the joker Irrelevant type. We also remove those
+    // constraints which require pointer types for the sockaddr param.
+    auto Accept =
+        Summary(NoEvalCall)
+            .Case(ReturnsFileDescriptor)
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)));
+    if (!addToFunctionSummaryMap(
+            "accept",
+            // int accept(int socket, struct sockaddr *restrict address,
+            //            socklen_t *restrict address_len);
+            Signature(ArgTypes{IntTy, StructSockaddrPtrRestrictTy,
+                               Socklen_tPtrRestrictTy},
+                      RetType{IntTy}),
+            Accept))
+      addToFunctionSummaryMap(
+          "accept",
+          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tPtrRestrictTy},
+                    RetType{IntTy}),
+          Accept);
+
+    // int bind(int socket, const struct sockaddr *address, socklen_t
+    //          address_len);
+    if (!addToFunctionSummaryMap(
+            "bind",
+            Signature(ArgTypes{IntTy, ConstStructSockaddrPtrTy, Socklen_tTy},
+                      RetType{IntTy}),
+            Summary(NoEvalCall)
+                .Case(ReturnsZeroOrMinusOne)
+                .ArgConstraint(
+                    ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+                .ArgConstraint(NotNull(ArgNo(1)))
+                .ArgConstraint(
+                    BufferSize(/*Buffer=*/ArgNo(1), /*BufSize=*/ArgNo(2)))
+                .ArgConstraint(
+                    ArgumentCondition(2, WithinRange, Range(0, Socklen_tMax)))))
+      // Do not add constraints on sockaddr.
       addToFunctionSummaryMap(
-          "mmap",
-          Summary(ArgTypes{VoidPtrTy, SizeTy, IntTy, IntTy, IntTy, *Off_tTy},
-                  RetType{VoidPtrTy}, NoEvalCall)
+          "bind",
+          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tTy}, RetType{IntTy}),
+          Summary(NoEvalCall)
+              .Case(ReturnsZeroOrMinusOne)
               .ArgConstraint(
-                  ArgumentCondition(1, WithinRange, Range(1, SizeMax)))
+                  ArgumentCondition(0, WithinRange, Range(0, IntMax)))
               .ArgConstraint(
-                  ArgumentCondition(4, WithinRange, Range(0, *Off_tMax))));
-    }
+                  ArgumentCondition(2, WithinRange, Range(0, Socklen_tMax))));
+
+    // int getpeername(int socket, struct sockaddr *restrict address,
+    //                 socklen_t *restrict address_len);
+    if (!addToFunctionSummaryMap(
+            "getpeername",
+            Signature(ArgTypes{IntTy, StructSockaddrPtrRestrictTy,
+                               Socklen_tPtrRestrictTy},
+                      RetType{IntTy}),
+            Summary(NoEvalCall)
+                .Case(ReturnsZeroOrMinusOne)
+                .ArgConstraint(
+                    ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+                .ArgConstraint(NotNull(ArgNo(1)))
+                .ArgConstraint(NotNull(ArgNo(2)))))
+      addToFunctionSummaryMap(
+          "getpeername",
+          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tPtrRestrictTy},
+                    RetType{IntTy}),
+          Summary(NoEvalCall)
+              .Case(ReturnsZeroOrMinusOne)
+              .ArgConstraint(
+                  ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-    Optional<QualType> Off64_tTy = lookupType("off64_t", ACtx);
-    Optional<RangeInt> Off64_tMax;
-    if (Off64_tTy) {
-      Off64_tMax = BVF.getMaxValue(*Off_tTy).getLimitedValue();
-      // void *mmap64(void *addr, size_t length, int prot, int flags, int fd,
-      // off64_t offset);
+    // int getsockname(int socket, struct sockaddr *restrict address,
+    //                 socklen_t *restrict address_len);
+    if (!addToFunctionSummaryMap(
+            "getsockname",
+            Signature(ArgTypes{IntTy, StructSockaddrPtrRestrictTy,
+                               Socklen_tPtrRestrictTy},
+                      RetType{IntTy}),
+            Summary(NoEvalCall)
+                .Case(ReturnsZeroOrMinusOne)
+                .ArgConstraint(
+                    ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+                .ArgConstraint(NotNull(ArgNo(1)))
+                .ArgConstraint(NotNull(ArgNo(2)))))
       addToFunctionSummaryMap(
-          "mmap64",
-          Summary(ArgTypes{VoidPtrTy, SizeTy, IntTy, IntTy, IntTy, *Off64_tTy},
-                  RetType{VoidPtrTy}, NoEvalCall)
+          "getsockname",
+          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tPtrRestrictTy},
+                    RetType{IntTy}),
+          Summary(NoEvalCall)
+              .Case(ReturnsZeroOrMinusOne)
               .ArgConstraint(
-                  ArgumentCondition(1, WithinRange, Range(1, SizeMax)))
+                  ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+
+    // int connect(int socket, const struct sockaddr *address, socklen_t
+    //             address_len);
+    if (!addToFunctionSummaryMap(
+            "connect",
+            Signature(ArgTypes{IntTy, ConstStructSockaddrPtrTy, Socklen_tTy},
+                      RetType{IntTy}),
+            Summary(NoEvalCall)
+                .Case(ReturnsZeroOrMinusOne)
+                .ArgConstraint(
+                    ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+                .ArgConstraint(NotNull(ArgNo(1)))))
+      addToFunctionSummaryMap(
+          "connect",
+          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tTy}, RetType{IntTy}),
+          Summary(NoEvalCall)
+              .Case(ReturnsZeroOrMinusOne)
               .ArgConstraint(
-                  ArgumentCondition(4, WithinRange, Range(0, *Off64_tMax))));
-    }
+                  ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-    // int pipe(int fildes[2]);
+    auto Recvfrom =
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
+                                      /*BufSize=*/ArgNo(2)));
+    if (!addToFunctionSummaryMap(
+            "recvfrom",
+            // ssize_t recvfrom(int socket, void *restrict buffer,
+            //                  size_t length,
+            //                  int flags, struct sockaddr *restrict address,
+            //                  socklen_t *restrict address_len);
+            Signature(ArgTypes{IntTy, VoidPtrRestrictTy, SizeTy, IntTy,
+                               StructSockaddrPtrRestrictTy,
+                               Socklen_tPtrRestrictTy},
+                      RetType{Ssize_tTy}),
+            Recvfrom))
+      addToFunctionSummaryMap(
+          "recvfrom",
+          Signature(ArgTypes{IntTy, VoidPtrRestrictTy, SizeTy, IntTy,
+                             Irrelevant, Socklen_tPtrRestrictTy},
+                    RetType{Ssize_tTy}),
+          Recvfrom);
+
+    auto Sendto =
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
+                                      /*BufSize=*/ArgNo(2)));
+    if (!addToFunctionSummaryMap(
+            "sendto",
+            // ssize_t sendto(int socket, const void *message, size_t length,
+            //                int flags, const struct sockaddr *dest_addr,
+            //                socklen_t dest_len);
+            Signature(ArgTypes{IntTy, ConstVoidPtrTy, SizeTy, IntTy,
+                               ConstStructSockaddrPtrTy, Socklen_tTy},
+                      RetType{Ssize_tTy}),
+            Sendto))
+      addToFunctionSummaryMap(
+          "sendto",
+          Signature(ArgTypes{IntTy, ConstVoidPtrTy, SizeTy, IntTy, Irrelevant,
+                             Socklen_tTy},
+                    RetType{Ssize_tTy}),
+          Sendto);
+
+    // int listen(int sockfd, int backlog);
+    addToFunctionSummaryMap("listen",
+                            Signature(ArgTypes{IntTy, IntTy}, RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(ArgumentCondition(
+                                    0, WithinRange, Range(0, IntMax))));
+
+    // ssize_t recv(int sockfd, void *buf, size_t len, int flags);
     addToFunctionSummaryMap(
-        "pipe", Summary(ArgTypes{IntPtrTy}, RetType{IntTy}, NoEvalCall)
-                    .ArgConstraint(NotNull(ArgNo(0))));
+        "recv",
+        Signature(ArgTypes{IntTy, VoidPtrTy, SizeTy, IntTy},
+                  RetType{Ssize_tTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
+                                      /*BufSize=*/ArgNo(2))));
 
-    if (Off_tTy)
-      // off_t lseek(int fildes, off_t offset, int whence);
-      addToFunctionSummaryMap(
-          "lseek", Summary(ArgTypes{IntTy, *Off_tTy, IntTy}, RetType{*Off_tTy},
-                           NoEvalCall)
-                       .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                        Range(0, IntMax))));
+    Optional<QualType> StructMsghdrTy = lookupTy("msghdr");
+    Optional<QualType> StructMsghdrPtrTy = getPointerTy(StructMsghdrTy);
+    Optional<QualType> ConstStructMsghdrPtrTy =
+        getPointerTy(getConstTy(StructMsghdrTy));
 
-    Optional<QualType> Ssize_tTy = lookupType("ssize_t", ACtx);
+    // ssize_t recvmsg(int sockfd, struct msghdr *msg, int flags);
+    addToFunctionSummaryMap(
+        "recvmsg",
+        Signature(ArgTypes{IntTy, StructMsghdrPtrTy, IntTy},
+                  RetType{Ssize_tTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-    if (Ssize_tTy) {
-      // ssize_t readlink(const char *restrict path, char *restrict buf,
-      //                  size_t bufsize);
-      addToFunctionSummaryMap(
-          "readlink",
-          Summary(ArgTypes{ConstCharPtrRestrictTy, CharPtrRestrictTy, SizeTy},
-                  RetType{*Ssize_tTy}, NoEvalCall)
-              .ArgConstraint(NotNull(ArgNo(0)))
-              .ArgConstraint(NotNull(ArgNo(1)))
-              .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
-                                        /*BufSize=*/ArgNo(2)))
-              .ArgConstraint(
-                  ArgumentCondition(2, WithinRange, Range(0, SizeMax))));
+    // ssize_t sendmsg(int sockfd, const struct msghdr *msg, int flags);
+    addToFunctionSummaryMap(
+        "sendmsg",
+        Signature(ArgTypes{IntTy, ConstStructMsghdrPtrTy, IntTy},
+                  RetType{Ssize_tTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
-      // ssize_t readlinkat(int fd, const char *restrict path,
-      //                    char *restrict buf, size_t bufsize);
-      addToFunctionSummaryMap(
-          "readlinkat", Summary(ArgTypes{IntTy, ConstCharPtrRestrictTy,
-                                         CharPtrRestrictTy, SizeTy},
-                                RetType{*Ssize_tTy}, NoEvalCall)
-                            .ArgConstraint(ArgumentCondition(0, WithinRange,
-                                                             Range(0, IntMax)))
-                            .ArgConstraint(NotNull(ArgNo(1)))
-                            .ArgConstraint(NotNull(ArgNo(2)))
-                            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(2),
-                                                      /*BufSize=*/ArgNo(3)))
-                            .ArgConstraint(ArgumentCondition(
-                                3, WithinRange, Range(0, SizeMax))));
-    }
+    // int setsockopt(int socket, int level, int option_name,
+    //                const void *option_value, socklen_t option_len);
+    addToFunctionSummaryMap(
+        "setsockopt",
+        Signature(ArgTypes{IntTy, IntTy, IntTy, ConstVoidPtrTy, Socklen_tTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(3)))
+            .ArgConstraint(
+                BufferSize(/*Buffer=*/ArgNo(3), /*BufSize=*/ArgNo(4)))
+            .ArgConstraint(
+                ArgumentCondition(4, WithinRange, Range(0, Socklen_tMax))));
 
-    // int renameat(int olddirfd, const char *oldpath, int newdirfd, const char
-    // *newpath);
-    addToFunctionSummaryMap("renameat", Summary(ArgTypes{IntTy, ConstCharPtrTy,
-                                                         IntTy, ConstCharPtrTy},
-                                                RetType{IntTy}, NoEvalCall)
-                                            .ArgConstraint(NotNull(ArgNo(1)))
-                                            .ArgConstraint(NotNull(ArgNo(3))));
+    // int getsockopt(int socket, int level, int option_name,
+    //                void *restrict option_value,
+    //                socklen_t *restrict option_len);
+    addToFunctionSummaryMap(
+        "getsockopt",
+        Signature(ArgTypes{IntTy, IntTy, IntTy, VoidPtrRestrictTy,
+                           Socklen_tPtrRestrictTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(3)))
+            .ArgConstraint(NotNull(ArgNo(4))));
+
+    // ssize_t send(int sockfd, const void *buf, size_t len, int flags);
+    addToFunctionSummaryMap(
+        "send",
+        Signature(ArgTypes{IntTy, ConstVoidPtrTy, SizeTy, IntTy},
+                  RetType{Ssize_tTy}),
+        Summary(NoEvalCall)
+            .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
+                                      /*BufSize=*/ArgNo(2))));
 
-    // char *realpath(const char *restrict file_name,
-    //                char *restrict resolved_name);
+    // int socketpair(int domain, int type, int protocol, int sv[2]);
+    addToFunctionSummaryMap(
+        "socketpair",
+        Signature(ArgTypes{IntTy, IntTy, IntTy, IntPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(3))));
+
+    // int getnameinfo(const struct sockaddr *restrict sa, socklen_t salen,
+    //                 char *restrict node, socklen_t nodelen,
+    //                 char *restrict service,
+    //                 socklen_t servicelen, int flags);
+    //
+    // This is defined in netdb.h. And contrary to 'socket.h', the sockaddr
+    // parameter is never handled as a transparent union in netdb.h
     addToFunctionSummaryMap(
-        "realpath", Summary(ArgTypes{ConstCharPtrRestrictTy, CharPtrRestrictTy},
-                            RetType{CharPtrTy}, NoEvalCall)
-                        .ArgConstraint(NotNull(ArgNo(0))));
+        "getnameinfo",
+        Signature(ArgTypes{ConstStructSockaddrPtrRestrictTy, Socklen_tTy,
+                           CharPtrRestrictTy, Socklen_tTy, CharPtrRestrictTy,
+                           Socklen_tTy, IntTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(
+                BufferSize(/*Buffer=*/ArgNo(0), /*BufSize=*/ArgNo(1)))
+            .ArgConstraint(
+                ArgumentCondition(1, WithinRange, Range(0, Socklen_tMax)))
+            .ArgConstraint(
+                BufferSize(/*Buffer=*/ArgNo(2), /*BufSize=*/ArgNo(3)))
+            .ArgConstraint(
+                ArgumentCondition(3, WithinRange, Range(0, Socklen_tMax)))
+            .ArgConstraint(
+                BufferSize(/*Buffer=*/ArgNo(4), /*BufSize=*/ArgNo(5)))
+            .ArgConstraint(
+                ArgumentCondition(5, WithinRange, Range(0, Socklen_tMax))));
 
-    QualType CharPtrConstPtr = ACtx.getPointerType(CharPtrTy.withConst());
+    Optional<QualType> StructUtimbufTy = lookupTy("utimbuf");
+    Optional<QualType> StructUtimbufPtrTy = getPointerTy(StructUtimbufTy);
 
-    // int execv(const char *path, char *const argv[]);
-    addToFunctionSummaryMap("execv",
-                            Summary(ArgTypes{ConstCharPtrTy, CharPtrConstPtr},
-                                    RetType{IntTy}, NoEvalCall)
-                                .ArgConstraint(NotNull(ArgNo(0))));
+    // int utime(const char *filename, struct utimbuf *buf);
+    addToFunctionSummaryMap(
+        "utime",
+        Signature(ArgTypes{ConstCharPtrTy, StructUtimbufPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
 
-    // int execvp(const char *file, char *const argv[]);
-    addToFunctionSummaryMap("execvp",
-                            Summary(ArgTypes{ConstCharPtrTy, CharPtrConstPtr},
-                                    RetType{IntTy}, NoEvalCall)
-                                .ArgConstraint(NotNull(ArgNo(0))));
+    Optional<QualType> StructTimespecTy = lookupTy("timespec");
+    Optional<QualType> StructTimespecPtrTy = getPointerTy(StructTimespecTy);
+    Optional<QualType> ConstStructTimespecPtrTy =
+        getPointerTy(getConstTy(StructTimespecTy));
 
-    // int getopt(int argc, char * const argv[], const char *optstring);
+    // int futimens(int fd, const struct timespec times[2]);
     addToFunctionSummaryMap(
-        "getopt",
-        Summary(ArgTypes{IntTy, CharPtrConstPtr, ConstCharPtrTy},
-                RetType{IntTy}, NoEvalCall)
-            .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
+        "futimens",
+        Signature(ArgTypes{IntTy, ConstStructTimespecPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(
+                ArgumentCondition(0, WithinRange, Range(0, IntMax))));
+
+    // int utimensat(int dirfd, const char *pathname,
+    //               const struct timespec times[2], int flags);
+    addToFunctionSummaryMap("utimensat",
+                            Signature(ArgTypes{IntTy, ConstCharPtrTy,
+                                               ConstStructTimespecPtrTy, IntTy},
+                                      RetType{IntTy}),
+                            Summary(NoEvalCall)
+                                .Case(ReturnsZeroOrMinusOne)
+                                .ArgConstraint(NotNull(ArgNo(1))));
+
+    Optional<QualType> StructTimevalTy = lookupTy("timeval");
+    Optional<QualType> ConstStructTimevalPtrTy =
+        getPointerTy(getConstTy(StructTimevalTy));
+
+    // int utimes(const char *filename, const struct timeval times[2]);
+    addToFunctionSummaryMap(
+        "utimes",
+        Signature(ArgTypes{ConstCharPtrTy, ConstStructTimevalPtrTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
+
+    // int nanosleep(const struct timespec *rqtp, struct timespec *rmtp);
+    addToFunctionSummaryMap(
+        "nanosleep",
+        Signature(ArgTypes{ConstStructTimespecPtrTy, StructTimespecPtrTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(0))));
+
+    Optional<QualType> Time_tTy = lookupTy("time_t");
+    Optional<QualType> ConstTime_tPtrTy = getPointerTy(getConstTy(Time_tTy));
+    Optional<QualType> ConstTime_tPtrRestrictTy =
+        getRestrictTy(ConstTime_tPtrTy);
+
+    Optional<QualType> StructTmTy = lookupTy("tm");
+    Optional<QualType> StructTmPtrTy = getPointerTy(StructTmTy);
+    Optional<QualType> StructTmPtrRestrictTy = getRestrictTy(StructTmPtrTy);
+    Optional<QualType> ConstStructTmPtrTy =
+        getPointerTy(getConstTy(StructTmTy));
+    Optional<QualType> ConstStructTmPtrRestrictTy =
+        getRestrictTy(ConstStructTmPtrTy);
+
+    // struct tm * localtime(const time_t *tp);
+    addToFunctionSummaryMap(
+        "localtime",
+        Signature(ArgTypes{ConstTime_tPtrTy}, RetType{StructTmPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // struct tm *localtime_r(const time_t *restrict timer,
+    //                        struct tm *restrict result);
+    addToFunctionSummaryMap(
+        "localtime_r",
+        Signature(ArgTypes{ConstTime_tPtrRestrictTy, StructTmPtrRestrictTy},
+                  RetType{StructTmPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
+
+    // char *asctime_r(const struct tm *restrict tm, char *restrict buf);
+    addToFunctionSummaryMap(
+        "asctime_r",
+        Signature(ArgTypes{ConstStructTmPtrRestrictTy, CharPtrRestrictTy},
+                  RetType{CharPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(1),
+                                      /*MinBufSize=*/BVF.getValue(26, IntTy))));
+
+    // char *ctime_r(const time_t *timep, char *buf);
+    addToFunctionSummaryMap(
+        "ctime_r",
+        Signature(ArgTypes{ConstTime_tPtrTy, CharPtrTy}, RetType{CharPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
             .ArgConstraint(NotNull(ArgNo(1)))
+            .ArgConstraint(BufferSize(
+                /*Buffer=*/ArgNo(1),
+                /*MinBufSize=*/BVF.getValue(26, IntTy))));
+
+    // struct tm *gmtime_r(const time_t *restrict timer,
+    //                     struct tm *restrict result);
+    addToFunctionSummaryMap(
+        "gmtime_r",
+        Signature(ArgTypes{ConstTime_tPtrRestrictTy, StructTmPtrRestrictTy},
+                  RetType{StructTmPtrTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
+
+    // struct tm * gmtime(const time_t *tp);
+    addToFunctionSummaryMap(
+        "gmtime", Signature(ArgTypes{ConstTime_tPtrTy}, RetType{StructTmPtrTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    Optional<QualType> Clockid_tTy = lookupTy("clockid_t");
+
+    // int clock_gettime(clockid_t clock_id, struct timespec *tp);
+    addToFunctionSummaryMap(
+        "clock_gettime",
+        Signature(ArgTypes{Clockid_tTy, StructTimespecPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(1))));
+
+    Optional<QualType> StructItimervalTy = lookupTy("itimerval");
+    Optional<QualType> StructItimervalPtrTy = getPointerTy(StructItimervalTy);
+
+    // int getitimer(int which, struct itimerval *curr_value);
+    addToFunctionSummaryMap(
+        "getitimer",
+        Signature(ArgTypes{IntTy, StructItimervalPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .Case(ReturnsZeroOrMinusOne)
+            .ArgConstraint(NotNull(ArgNo(1))));
+
+    Optional<QualType> Pthread_cond_tTy = lookupTy("pthread_cond_t");
+    Optional<QualType> Pthread_cond_tPtrTy = getPointerTy(Pthread_cond_tTy);
+    Optional<QualType> Pthread_tTy = lookupTy("pthread_t");
+    Optional<QualType> Pthread_tPtrTy = getPointerTy(Pthread_tTy);
+    Optional<QualType> Pthread_tPtrRestrictTy = getRestrictTy(Pthread_tPtrTy);
+    Optional<QualType> Pthread_mutex_tTy = lookupTy("pthread_mutex_t");
+    Optional<QualType> Pthread_mutex_tPtrTy = getPointerTy(Pthread_mutex_tTy);
+    Optional<QualType> Pthread_mutex_tPtrRestrictTy =
+        getRestrictTy(Pthread_mutex_tPtrTy);
+    Optional<QualType> Pthread_attr_tTy = lookupTy("pthread_attr_t");
+    Optional<QualType> Pthread_attr_tPtrTy = getPointerTy(Pthread_attr_tTy);
+    Optional<QualType> ConstPthread_attr_tPtrTy =
+        getPointerTy(getConstTy(Pthread_attr_tTy));
+    Optional<QualType> ConstPthread_attr_tPtrRestrictTy =
+        getRestrictTy(ConstPthread_attr_tPtrTy);
+    Optional<QualType> Pthread_mutexattr_tTy = lookupTy("pthread_mutexattr_t");
+    Optional<QualType> ConstPthread_mutexattr_tPtrTy =
+        getPointerTy(getConstTy(Pthread_mutexattr_tTy));
+    Optional<QualType> ConstPthread_mutexattr_tPtrRestrictTy =
+        getRestrictTy(ConstPthread_mutexattr_tPtrTy);
+
+    QualType PthreadStartRoutineTy = getPointerTy(
+        ACtx.getFunctionType(/*ResultTy=*/VoidPtrTy, /*Args=*/VoidPtrTy,
+                             FunctionProtoType::ExtProtoInfo()));
+
+    // int pthread_cond_signal(pthread_cond_t *cond);
+    // int pthread_cond_broadcast(pthread_cond_t *cond);
+    addToFunctionSummaryMap(
+        {"pthread_cond_signal", "pthread_cond_broadcast"},
+        Signature(ArgTypes{Pthread_cond_tPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // int pthread_create(pthread_t *restrict thread,
+    //                    const pthread_attr_t *restrict attr,
+    //                    void *(*start_routine)(void*), void *restrict arg);
+    addToFunctionSummaryMap(
+        "pthread_create",
+        Signature(ArgTypes{Pthread_tPtrRestrictTy,
+                           ConstPthread_attr_tPtrRestrictTy,
+                           PthreadStartRoutineTy, VoidPtrRestrictTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
             .ArgConstraint(NotNull(ArgNo(2))));
+
+    // int pthread_attr_destroy(pthread_attr_t *attr);
+    // int pthread_attr_init(pthread_attr_t *attr);
+    addToFunctionSummaryMap(
+        {"pthread_attr_destroy", "pthread_attr_init"},
+        Signature(ArgTypes{Pthread_attr_tPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // int pthread_attr_getstacksize(const pthread_attr_t *restrict attr,
+    //                               size_t *restrict stacksize);
+    // int pthread_attr_getguardsize(const pthread_attr_t *restrict attr,
+    //                               size_t *restrict guardsize);
+    addToFunctionSummaryMap(
+        {"pthread_attr_getstacksize", "pthread_attr_getguardsize"},
+        Signature(ArgTypes{ConstPthread_attr_tPtrRestrictTy, SizePtrRestrictTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
+
+    // int pthread_attr_setstacksize(pthread_attr_t *attr, size_t stacksize);
+    // int pthread_attr_setguardsize(pthread_attr_t *attr, size_t guardsize);
+    addToFunctionSummaryMap(
+        {"pthread_attr_setstacksize", "pthread_attr_setguardsize"},
+        Signature(ArgTypes{Pthread_attr_tPtrTy, SizeTy}, RetType{IntTy}),
+        Summary(NoEvalCall)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(
+                ArgumentCondition(1, WithinRange, Range(0, SizeMax))));
+
+    // int pthread_mutex_init(pthread_mutex_t *restrict mutex, const
+    //                        pthread_mutexattr_t *restrict attr);
+    addToFunctionSummaryMap(
+        "pthread_mutex_init",
+        Signature(ArgTypes{Pthread_mutex_tPtrRestrictTy,
+                           ConstPthread_mutexattr_tPtrRestrictTy},
+                  RetType{IntTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
+
+    // int pthread_mutex_destroy(pthread_mutex_t *mutex);
+    // int pthread_mutex_lock(pthread_mutex_t *mutex);
+    // int pthread_mutex_trylock(pthread_mutex_t *mutex);
+    // int pthread_mutex_unlock(pthread_mutex_t *mutex);
+    addToFunctionSummaryMap(
+        {"pthread_mutex_destroy", "pthread_mutex_lock", "pthread_mutex_trylock",
+         "pthread_mutex_unlock"},
+        Signature(ArgTypes{Pthread_mutex_tPtrTy}, RetType{IntTy}),
+        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
   }
 
   // Functions for testing.
   if (ChecksEnabled[CK_StdCLibraryFunctionsTesterChecker]) {
     addToFunctionSummaryMap(
         "__two_constrained_args",
-        Summary(ArgTypes{IntTy, IntTy}, RetType{IntTy}, EvalCallAsPure)
+        Signature(ArgTypes{IntTy, IntTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure)
             .ArgConstraint(ArgumentCondition(0U, WithinRange, SingleValue(1)))
             .ArgConstraint(ArgumentCondition(1U, WithinRange, SingleValue(1))));
     addToFunctionSummaryMap(
-        "__arg_constrained_twice",
-        Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
+        "__arg_constrained_twice", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure)
             .ArgConstraint(ArgumentCondition(0U, OutOfRange, SingleValue(1)))
             .ArgConstraint(ArgumentCondition(0U, OutOfRange, SingleValue(2))));
     addToFunctionSummaryMap(
         "__defaultparam",
-        Summary(ArgTypes{Irrelevant, IntTy}, RetType{IntTy}, EvalCallAsPure)
-            .ArgConstraint(NotNull(ArgNo(0))));
-    addToFunctionSummaryMap("__variadic",
-                            Summary(ArgTypes{VoidPtrTy, ConstCharPtrTy},
-                                    RetType{IntTy}, EvalCallAsPure)
-                                .ArgConstraint(NotNull(ArgNo(0)))
-                                .ArgConstraint(NotNull(ArgNo(1))));
+        Signature(ArgTypes{Irrelevant, IntTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure).ArgConstraint(NotNull(ArgNo(0))));
+    addToFunctionSummaryMap(
+        "__variadic",
+        Signature(ArgTypes{VoidPtrTy, ConstCharPtrTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure)
+            .ArgConstraint(NotNull(ArgNo(0)))
+            .ArgConstraint(NotNull(ArgNo(1))));
     addToFunctionSummaryMap(
         "__buf_size_arg_constraint",
-        Summary(ArgTypes{ConstVoidPtrTy, SizeTy}, RetType{IntTy},
-                EvalCallAsPure)
+        Signature(ArgTypes{ConstVoidPtrTy, SizeTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure)
             .ArgConstraint(
                 BufferSize(/*Buffer=*/ArgNo(0), /*BufSize=*/ArgNo(1))));
     addToFunctionSummaryMap(
         "__buf_size_arg_constraint_mul",
-        Summary(ArgTypes{ConstVoidPtrTy, SizeTy, SizeTy}, RetType{IntTy},
-                EvalCallAsPure)
+        Signature(ArgTypes{ConstVoidPtrTy, SizeTy, SizeTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure)
             .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(0), /*BufSize=*/ArgNo(1),
                                       /*BufSizeMultiplier=*/ArgNo(2))));
+    addToFunctionSummaryMap(
+        "__buf_size_arg_constraint_concrete",
+        Signature(ArgTypes{ConstVoidPtrTy}, RetType{IntTy}),
+        Summary(EvalCallAsPure)
+            .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(0),
+                                      /*BufSize=*/BVF.getValue(10, IntTy))));
+    addToFunctionSummaryMap(
+        {"__test_restrict_param_0", "__test_restrict_param_1",
+         "__test_restrict_param_2"},
+        Signature(ArgTypes{VoidPtrRestrictTy}, RetType{VoidTy}),
+        Summary(EvalCallAsPure));
   }
 }
 
@@ -1749,7 +2496,8 @@ void ento::registerStdCLibraryFunctionsChecker(CheckerManager &mgr) {
       mgr.getAnalyzerOptions().getCheckerBooleanOption(Checker, "ModelPOSIX");
 }
 
-bool ento::shouldRegisterStdCLibraryFunctionsChecker(const CheckerManager &mgr) {
+bool ento::shouldRegisterStdCLibraryFunctionsChecker(
+    const CheckerManager &mgr) {
   return true;
 }