void StdLibraryFunctionsChecker::initFunctionSummaries()

in clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp [950:2659]


void StdLibraryFunctionsChecker::initFunctionSummaries(
    CheckerContext &C) const {
  if (SummariesInitialized)
    return;

  SValBuilder &SVB = C.getSValBuilder();
  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.empty())
        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".
  // In such cases it should be possible to provide multiple variants
  // of function summary for common cases (eg. ssize_t could be int or long
  // 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 SizeTy = ACtx.getSizeType();

  const QualType VoidPtrTy = getPointerTy(VoidTy); // void *
  const QualType IntPtrTy = getPointerTy(IntTy);   // int *
  const QualType UnsignedIntPtrTy =
      getPointerTy(UnsignedIntTy); // unsigned int *
  const QualType VoidPtrRestrictTy = getRestrictTy(VoidPtrTy);
  const QualType ConstVoidPtrTy =
      getPointerTy(getConstTy(VoidTy));            // const void *
  const QualType CharPtrTy = getPointerTy(CharTy); // char *
  const QualType CharPtrRestrictTy = getRestrictTy(CharPtrTy);
  const QualType ConstCharPtrTy =
      getPointerTy(getConstTy(CharTy)); // const char *
  const QualType ConstCharPtrRestrictTy = getRestrictTy(ConstCharPtrTy);
  const QualType Wchar_tPtrTy = getPointerTy(WCharTy); // wchar_t *
  const QualType ConstWchar_tPtrTy =
      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 SizeMax = BVF.getMaxValue(SizeTy).getLimitedValue();

  // Set UCharRangeMax to min of int or uchar maximum value.
  // The C standard states that the arguments of functions like isalpha must
  // be representable as an unsigned char. Their type is 'int', so the max
  // value of the argument should be min(UCharMax, IntMax). This just happen
  // to be true for commonly used and well tested instruction set
  // architectures, but not for others.
  const RangeInt UCharRangeMax =
      std::min(BVF.getMaxValue(ACtx.UnsignedCharTy).getLimitedValue(), IntMax);

  // The platform dependent value of EOF.
  // Try our best to parse this from the Preprocessor, otherwise fallback to -1.
  const auto EOFv = [&C]() -> RangeInt {
    if (const llvm::Optional<int> OptInt =
            tryExpandAsInteger("EOF", C.getPreprocessor()))
      return *OptInt;
    return -1;
  }();

  // Auxiliary class to aid adding summaries to the summary map.
  struct AddToFunctionSummaryMap {
    const ASTContext &ACtx;
    FunctionSummaryMapType &Map;
    bool DisplayLoadedSummaries;
    AddToFunctionSummaryMap(const ASTContext &ACtx, FunctionSummaryMapType &FSM,
                            bool DisplayLoadedSummaries)
        : ACtx(ACtx), Map(FSM), DisplayLoadedSummaries(DisplayLoadedSummaries) {
    }

    // 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.
    //
    // 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.empty())
        return false;
      for (Decl *D : LookupRes) {
        if (auto *FD = dyn_cast<FunctionDecl>(D)) {
          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) {
              llvm::errs() << "Loaded summary for: ";
              FD->print(llvm::errs());
              llvm::errs() << "\n";
            }
            return true;
          }
        }
      }
      return false;
    }
    // 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);

  // Below are helpers functions to create the summaries.
  auto ArgumentCondition = [](ArgNo ArgN, RangeKind Kind,
                              IntRangeVector Ranges) {
    return std::make_shared<RangeConstraint>(ArgN, Kind, Ranges);
  };
  auto BufferSize = [](auto... Args) {
    return std::make_shared<BufferSizeConstraint>(Args...);
  };
  struct {
    auto operator()(RangeKind Kind, IntRangeVector Ranges) {
      return std::make_shared<RangeConstraint>(Ret, Kind, Ranges);
    }
    auto operator()(BinaryOperator::Opcode Op, ArgNo OtherArgN) {
      return std::make_shared<ComparisonConstraint>(Ret, Op, OtherArgN);
    }
  } ReturnValueCondition;
  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}};
  };
  auto LessThanOrEq = BO_LE;
  auto NotNull = [&](ArgNo ArgN) {
    return std::make_shared<NotNullConstraint>(ArgN);
  };

  Optional<QualType> FileTy = lookupTy("FILE");
  Optional<QualType> FilePtrTy = getPointerTy(FileTy);
  Optional<QualType> FilePtrRestrictTy = getRestrictTy(FilePtrTy);

  // 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", 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'}}),
                 ReturnValueCondition(OutOfRange, SingleValue(0))})
          // The locale-specific range.
          // No post-condition. We are completely unaware of
          // locale-specific return values.
          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
          .Case(
              {ArgumentCondition(
                   0U, OutOfRange,
                   {{'0', '9'}, {'A', 'Z'}, {'a', 'z'}, {128, UCharRangeMax}}),
               ReturnValueCondition(WithinRange, SingleValue(0))})
          .ArgConstraint(ArgumentCondition(
              0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
  addToFunctionSummaryMap(
      "isalpha", Signature(ArgTypes{IntTy}, RetType{IntTy}),
      Summary(EvalCallAsPure)
          .Case({ArgumentCondition(0U, WithinRange, {{'A', 'Z'}, {'a', 'z'}}),
                 ReturnValueCondition(OutOfRange, SingleValue(0))})
          // The locale-specific range.
          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
          .Case({ArgumentCondition(
                     0U, OutOfRange,
                     {{'A', 'Z'}, {'a', 'z'}, {128, UCharRangeMax}}),
                 ReturnValueCondition(WithinRange, SingleValue(0))}));
  addToFunctionSummaryMap(
      "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", 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", 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", 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", 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", Signature(ArgTypes{IntTy}, RetType{IntTy}),
      Summary(EvalCallAsPure)
          // Is certainly lowercase.
          .Case({ArgumentCondition(0U, WithinRange, Range('a', 'z')),
                 ReturnValueCondition(OutOfRange, SingleValue(0))})
          // Is ascii but not lowercase.
          .Case({ArgumentCondition(0U, WithinRange, Range(0, 127)),
                 ArgumentCondition(0U, OutOfRange, Range('a', 'z')),
                 ReturnValueCondition(WithinRange, SingleValue(0))})
          // The locale-specific range.
          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
          // Is not an unsigned char.
          .Case({ArgumentCondition(0U, OutOfRange, Range(0, UCharRangeMax)),
                 ReturnValueCondition(WithinRange, SingleValue(0))}));
  addToFunctionSummaryMap(
      "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", Signature(ArgTypes{IntTy}, RetType{IntTy}),
      Summary(EvalCallAsPure)
          .Case({ArgumentCondition(
                     0U, WithinRange,
                     {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}),
                 ReturnValueCondition(OutOfRange, SingleValue(0))})
          .Case({ArgumentCondition(
                     0U, OutOfRange,
                     {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}),
                 ReturnValueCondition(WithinRange, SingleValue(0))}));
  addToFunctionSummaryMap(
      "isspace", Signature(ArgTypes{IntTy}, RetType{IntTy}),
      Summary(EvalCallAsPure)
          // Space, '\f', '\n', '\r', '\t', '\v'.
          .Case({ArgumentCondition(0U, WithinRange, {{9, 13}, {' ', ' '}}),
                 ReturnValueCondition(OutOfRange, SingleValue(0))})
          // The locale-specific range.
          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
          .Case({ArgumentCondition(0U, OutOfRange,
                                   {{9, 13}, {' ', ' '}, {128, UCharRangeMax}}),
                 ReturnValueCondition(WithinRange, SingleValue(0))}));
  addToFunctionSummaryMap(
      "isupper", Signature(ArgTypes{IntTy}, RetType{IntTy}),
      Summary(EvalCallAsPure)
          // Is certainly uppercase.
          .Case({ArgumentCondition(0U, WithinRange, Range('A', 'Z')),
                 ReturnValueCondition(OutOfRange, SingleValue(0))})
          // The locale-specific range.
          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
          // Other.
          .Case({ArgumentCondition(0U, OutOfRange,
                                   {{'A', 'Z'}, {128, UCharRangeMax}}),
                 ReturnValueCondition(WithinRange, SingleValue(0))}));
  addToFunctionSummaryMap(
      "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.
  addToFunctionSummaryMap(
      {"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.
  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))});

  // 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.
  // 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.
  // 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);

  {
    Summary GetenvSummary = Summary(NoEvalCall)
                                .ArgConstraint(NotNull(ArgNo(0)))
                                .Case({NotNull(Ret)});
    // In untrusted environments the envvar might not exist.
    if (!ShouldAssumeControlledEnvironment)
      GetenvSummary.Case({NotNull(Ret)->negate()});

    // char *getenv(const char *name);
    addToFunctionSummaryMap(
        "getenv", Signature(ArgTypes{ConstCharPtrTy}, RetType{CharPtrTy}),
        std::move(GetenvSummary));
  }

  if (ModelPOSIX) {

    // long a64l(const char *str64);
    addToFunctionSummaryMap(
        "a64l", Signature(ArgTypes{ConstCharPtrTy}, RetType{LongTy}),
        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));

    // char *l64a(long value);
    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", 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",
        Signature(ArgTypes{IntTy, ConstCharPtrTy, IntTy, IntTy},
                  RetType{IntTy}),
        Summary(NoEvalCall)
            .Case(ReturnsZeroOrMinusOne)
            .ArgConstraint(NotNull(ArgNo(1))));

    // int dup(int fildes);
    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", 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",
                            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",
        Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy, IntTy},
                  RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(NotNull(ArgNo(0)))
            .ArgConstraint(NotNull(ArgNo(1))));

    // int fsync(int fildes);
    addToFunctionSummaryMap("fsync", Signature(ArgTypes{IntTy}, RetType{IntTy}),
                            Summary(NoEvalCall)
                                .Case(ReturnsZeroOrMinusOne)
                                .ArgConstraint(ArgumentCondition(
                                    0, WithinRange, Range(0, IntMax))));

    Optional<QualType> Off_tTy = lookupTy("off_t");

    // 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",
        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",
        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))));

    // 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 = lookupTy("mode_t");

    // 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", Signature(ArgTypes{UnsignedIntTy}, RetType{UnsignedIntTy}),
        Summary(NoEvalCall)
            .ArgConstraint(
                ArgumentCondition(0, WithinRange, Range(0, UnsignedIntMax))));

    Optional<QualType> DirTy = lookupTy("DIR");
    Optional<QualType> DirPtrTy = getPointerTy(DirTy);

    // 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", Signature(ArgTypes{UnsignedIntTy}, RetType{UnsignedIntTy}),
        Summary(NoEvalCall)
            .ArgConstraint(
                ArgumentCondition(0, WithinRange, Range(0, UnsignedIntMax))));

    // 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", Signature(ArgTypes{ConstCharPtrTy}, RetType{CharPtrTy}),
        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));

    // char *strndup(const char *s, size_t n);
    addToFunctionSummaryMap(
        "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", Signature(ArgTypes{ConstWchar_tPtrTy}, RetType{Wchar_tPtrTy}),
        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));

    // int mkstemp(char *template);
    addToFunctionSummaryMap("mkstemp",
                            Signature(ArgTypes{CharPtrTy}, RetType{IntTy}),
                            Summary(NoEvalCall)
                                .Case(ReturnsFileDescriptor)
                                .ArgConstraint(NotNull(ArgNo(0))));

    // char *mkdtemp(char *template);
    addToFunctionSummaryMap(
        "mkdtemp", Signature(ArgTypes{CharPtrTy}, RetType{CharPtrTy}),
        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));

    // char *getcwd(char *buf, size_t size);
    addToFunctionSummaryMap(
        "getcwd", Signature(ArgTypes{CharPtrTy, SizeTy}, RetType{CharPtrTy}),
        Summary(NoEvalCall)
            .ArgConstraint(
                ArgumentCondition(1, WithinRange, Range(0, SizeMax))));

    // 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",
        Signature(ArgTypes{IntTy, ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
        Summary(NoEvalCall)
            .Case(ReturnsZeroOrMinusOne)
            .ArgConstraint(NotNull(ArgNo(1))));

    Optional<QualType> Dev_tTy = lookupTy("dev_t");

    // 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))));

    // 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 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 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))));

    // 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))));

    Optional<QualType> Uid_tTy = lookupTy("uid_t");
    Optional<QualType> Gid_tTy = lookupTy("gid_t");

    // 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 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 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 fchown(int fildes, uid_t owner, gid_t group);
    addToFunctionSummaryMap(
        "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",
                            Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
                            Summary(NoEvalCall)
                                .Case(ReturnsZeroOrMinusOne)
                                .ArgConstraint(NotNull(ArgNo(0))));

    // int link(const char *oldpath, const char *newpath);
    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",
        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",
                            Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
                            Summary(NoEvalCall)
                                .Case(ReturnsZeroOrMinusOne)
                                .ArgConstraint(NotNull(ArgNo(0))));

    // int unlinkat(int fd, const char *path, int flag);
    addToFunctionSummaryMap(
        "unlinkat",
        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 = lookupTy("stat");
    Optional<QualType> StructStatPtrTy = getPointerTy(StructStatTy);
    Optional<QualType> StructStatPtrRestrictTy = getRestrictTy(StructStatPtrTy);

    // 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))));

    // 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",
        Signature(ArgTypes{ConstCharPtrRestrictTy, StructStatPtrRestrictTy},
                  RetType{IntTy}),
        Summary(NoEvalCall)
            .Case(ReturnsZeroOrMinusOne)
            .ArgConstraint(NotNull(ArgNo(0)))
            .ArgConstraint(NotNull(ArgNo(1))));

    // 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 *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", Signature(ArgTypes{IntTy}, RetType{IntTy}),
        Summary(NoEvalCall)
            .Case({ReturnValueCondition(WithinRange, Range(0, 1))})
            .ArgConstraint(
                ArgumentCondition(0, WithinRange, Range(0, IntMax))));

    // 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", Signature(ArgTypes{FilePtrTy}, RetType{IntTy}),
        Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));

    // int close(int fildes);
    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",
                            Signature(ArgTypes{IntTy, IntTy}, RetType{LongTy}),
                            Summary(NoEvalCall)
                                .ArgConstraint(ArgumentCondition(
                                    0, WithinRange, Range(0, IntMax))));

    // long pathconf(const char *path, int name);
    addToFunctionSummaryMap(
        "pathconf", Signature(ArgTypes{ConstCharPtrTy, IntTy}, RetType{LongTy}),
        Summary(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 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", 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 fseeko(FILE *stream, off_t offset, int whence);
    addToFunctionSummaryMap(
        "fseeko",
        Signature(ArgTypes{FilePtrTy, Off_tTy, IntTy}, RetType{IntTy}),
        Summary(NoEvalCall)
            .Case(ReturnsZeroOrMinusOne)
            .ArgConstraint(NotNull(ArgNo(0))));

    // off_t ftello(FILE *stream);
    addToFunctionSummaryMap(
        "ftello", Signature(ArgTypes{FilePtrTy}, RetType{Off_tTy}),
        Summary(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))));

    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))));

    // 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))));

    // 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))));

    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(
          "bind",
          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tTy}, RetType{IntTy}),
          Summary(NoEvalCall)
              .Case(ReturnsZeroOrMinusOne)
              .ArgConstraint(
                  ArgumentCondition(0, WithinRange, Range(0, IntMax)))
              .ArgConstraint(
                  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))));

    // 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(
          "getsockname",
          Signature(ArgTypes{IntTy, Irrelevant, Socklen_tPtrRestrictTy},
                    RetType{IntTy}),
          Summary(NoEvalCall)
              .Case(ReturnsZeroOrMinusOne)
              .ArgConstraint(
                  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(0, WithinRange, Range(0, IntMax))));

    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(
        "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))));

    Optional<QualType> StructMsghdrTy = lookupTy("msghdr");
    Optional<QualType> StructMsghdrPtrTy = getPointerTy(StructMsghdrTy);
    Optional<QualType> ConstStructMsghdrPtrTy =
        getPointerTy(getConstTy(StructMsghdrTy));

    // 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))));

    // 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))));

    // 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 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))));

    // 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(
        "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))));

    Optional<QualType> StructUtimbufTy = lookupTy("utimbuf");
    Optional<QualType> StructUtimbufPtrTy = getPointerTy(StructUtimbufTy);

    // int utime(const char *filename, struct utimbuf *buf);
    addToFunctionSummaryMap(
        "utime",
        Signature(ArgTypes{ConstCharPtrTy, StructUtimbufPtrTy}, RetType{IntTy}),
        Summary(NoEvalCall)
            .Case(ReturnsZeroOrMinusOne)
            .ArgConstraint(NotNull(ArgNo(0))));

    Optional<QualType> StructTimespecTy = lookupTy("timespec");
    Optional<QualType> StructTimespecPtrTy = getPointerTy(StructTimespecTy);
    Optional<QualType> ConstStructTimespecPtrTy =
        getPointerTy(getConstTy(StructTimespecTy));

    // int futimens(int fd, const struct timespec times[2]);
    addToFunctionSummaryMap(
        "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(
        "__not_null", Signature(ArgTypes{IntPtrTy}, RetType{IntTy}),
        Summary(EvalCallAsPure).ArgConstraint(NotNull(ArgNo(0))));

    // Test range values.
    addToFunctionSummaryMap(
        "__single_val_1", Signature(ArgTypes{IntTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(ArgumentCondition(0U, WithinRange, SingleValue(1))));
    addToFunctionSummaryMap(
        "__range_1_2", Signature(ArgTypes{IntTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(ArgumentCondition(0U, WithinRange, Range(1, 2))));
    addToFunctionSummaryMap("__range_1_2__4_5",
                            Signature(ArgTypes{IntTy}, RetType{IntTy}),
                            Summary(EvalCallAsPure)
                                .ArgConstraint(ArgumentCondition(
                                    0U, WithinRange, Range({1, 2}, {4, 5}))));

    // Test range kind.
    addToFunctionSummaryMap(
        "__within", Signature(ArgTypes{IntTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(ArgumentCondition(0U, WithinRange, SingleValue(1))));
    addToFunctionSummaryMap(
        "__out_of", Signature(ArgTypes{IntTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(ArgumentCondition(0U, OutOfRange, SingleValue(1))));

    addToFunctionSummaryMap(
        "__two_constrained_args",
        Signature(ArgTypes{IntTy, IntTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(ArgumentCondition(0U, WithinRange, SingleValue(1)))
            .ArgConstraint(ArgumentCondition(1U, WithinRange, SingleValue(1))));
    addToFunctionSummaryMap(
        "__arg_constrained_twice", Signature(ArgTypes{IntTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(ArgumentCondition(0U, OutOfRange, SingleValue(1)))
            .ArgConstraint(ArgumentCondition(0U, OutOfRange, SingleValue(2))));
    addToFunctionSummaryMap(
        "__defaultparam",
        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",
        Signature(ArgTypes{ConstVoidPtrTy, SizeTy}, RetType{IntTy}),
        Summary(EvalCallAsPure)
            .ArgConstraint(
                BufferSize(/*Buffer=*/ArgNo(0), /*BufSize=*/ArgNo(1))));
    addToFunctionSummaryMap(
        "__buf_size_arg_constraint_mul",
        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));
  }

  SummariesInitialized = true;
}