[clang][Analyzer] Add errno state to standard functions modeling.

[balazske]

Summary

This updates StdLibraryFunctionsChecker to set the state of 'errno'
by using the new errno_modeling functionality.
The errno value is set in the PostCall callback. Setting it in call::Eval
did not work for some reason and then every function should be
EvalCallAsPure which may be bad to do. Now the errno value and state
is not allowed to be checked in any PostCall checker callback because
it is unspecified if the errno was set already or will be set later
by this checker.

[martong]

Nice work! Could you pleas add some lit tests that describe an errno related bugreport for a standard lib function?

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

394

This class serves as a base class, it is not really a Kind class which is usually just an enum.
I'd prefer to call this ErrnoConstraintBase or BasicErrnoConstraint.

396

This class is a polymorphic base class, since we have this virtual function here. Would make sense to make destructor virtual as well, even though delete is not called explicitly on the base class (as I see).

410

Please document the subclasses.

642–644

Would it make sense to have a ErrnoIrrelevant as the default value for ErrnoC?

758–761

Could you please add some more documentation to these variables? And they could be const.

[martong]

The bugreports look promising. However, I think we desperately need a note that describes which function has set the errno_modeling state. Below I'd expect the following notes for the highlighted function call.

• assuming return value of mkdir is in range [0, INT_MAX]
• errno is not set

I suppose, you'd need to add some changes for these both in the ErrnoChecker and here as well.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

448

Please check if State can be nullptr.

[balazske]

Function mkdir is modeled incorrectly by the checker. According to the man page it can return 0 or -1 only (-1 is error) but the checker allows non-negative value at success. So the shown bug report is incorrect (it can be only -1 if not 0 and then check of errno is allowed). Anyway the note tags should be added to every function.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

1751

These strings are for test purposes only.

[balazske]

@martong Do you mean that a "describe" function is needed for the return value constraint of the function and for the errno constraint type? Then a note tag can contain what the function is assumed to return on success and what is allowed (or not) to do with errno. For example: "Assuming that 'mkdir' is successful, it returns zero in this case and value of 'errno' is unspecified after the call".

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

448

I think here it is never null. A relation is created between a new conjured symbol and zero, this can never fail, or not? (The ErrnoSVal should be here a newly created symbol. If the Tag is not used it may be the same symbol that was previously bound to the expression if EvalCallAsPure is used.)

642–644

It would be a bit more convenient but in the current design it is not possible to pass the member variable as default value. ErrnoIrrelevant is really used in less than half of the cases.

[martong]

In D125400#3508955, @balazske wrote:

Function mkdir is modeled incorrectly by the checker. According to the man page it can return 0 or -1 only (-1 is error) but the checker allows non-negative value at success. So the shown bug report is incorrect (it can be only -1 if not 0 and then check of errno is allowed). Anyway the note tags should be added to every function.

Okay, could you please correct the summary then?

[martong]

In D125400#3516164, @balazske wrote:

@martong Do you mean that a "describe" function is needed for the return value constraint of the function and for the errno constraint type? Then a note tag can contain what the function is assumed to return on success and what is allowed (or not) to do with errno. For example: "Assuming that 'mkdir' is successful, it returns zero in this case and value of 'errno' is unspecified after the call".

Yes, that sounds good. We have the virtual describe function in the base constraint class that could be used to explain what values we expect.

[martong]

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

448

Okay, I see your reasoning. However, we might never know how the constraint solver reasons about it, thus we should not rely on that. As a contrived example, it might check recursively that the LHS of the BinOp you just conjured and it might recognize that the State is infeasible.

642–644

Ok.

[balazske]

added comments. added note tag, added test, improved the code

[steakhal]

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

406

425

The explicit qualification is not necessary. There are other cases like this.

In the constraint manager, we tend to use Op for operator kinds, it would be nice to use the same taxonomy here.

430

443–446

Just use .castAs<NonLoc>(). You will assert it anyway, and I find this much more readable.

454–460

I believe you should use Twine for this.

1024

What is <unknown> in this context? Please add a test for it or remove this branch.

1033–1038

Why did you change these?

clang/test/Analysis/errno-stdlibraryfunctions.c

21–25

29

[balazske]

update

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

454–460

It should work, FunctionName.str() and getOpcodeStr and describeErrnoCheckState should return non-temporary strings.

[balazske]

fixed some problems

[martong]

Nice work, looks promising! Once the test file related comment is addressed I will accept.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

2267

You mean the enforced errno check could cause false positive?

clang/test/Analysis/errno-stdlibraryfunctions.c

21–25

+1 for @steakhal's recommendation.

[balazske]

applied the review comments

[balazske]

rebase

[martong]

LGTM!

[balazske]

small test change, removed a compile warning

[martong]

clang/test/Analysis/errno-stdlibraryfunctions-notes.c

11 ↗

(On Diff #435082)

Do you plan to extend the test file for other standard functions as well?

clang/test/Analysis/errno-stdlibraryfunctions.c

15–16

Do you plan to extend the test file for other standard functions as well?

44–45

This should be reachable as well, isn't it?

[balazske]

clang/test/Analysis/errno-stdlibraryfunctions-notes.c

11 ↗

(On Diff #435082)

It was not planned. I am not sure if it is better to have some more functions but not all. If there is a test for all of the functions it should be generated somehow (test every function for success and failure case, arguments passed to the functions are probably not easy to generate).

[balazske]

small fix in test

[steakhal]

It's getting in really good shape. Nice work.
I've got some nits about docs and checker dependencies and also a major comment inline.

The documentation needs to be updated to keep it in sync.
It should demonstrate the new warnings, state why we have them. Remember to refer back to the CERT rule for additional resources.
Refer to the related checker, in this case to ErrnoModeling, and explain how it changes the analysis.
Shouldn't it be a modeling dependency rather?

clang/test/Analysis/errno-stdlibraryfunctions-notes.c

15–23 ↗

(On Diff #435558)

I must say that I dislike that one cannot disable this warning unless they disable the whole stdlibrarymodeling. It's getting bigger and bigger, thus increasing the value it provides. Yet, not everybody wants to follow SEI CERT guidelines - and I would expect plenty of users in that category, who might be surprised that reading errno is a bug.

Just imagine in the example that between the two access() calls, you set errno to zero.
The code would look reasonable.

1. reset errno
2. do some syscall
3. check errno

I would expect this to be a good practice. We should at least have an option for suppressing reports for such scenarios. IMO it should be rather opt-in, than opt-out, but it might be my personal preference.
WDYT @martong @xazax.hun

[balazske]

The documentation of ErrnoChecker is added in the previous change D122150. Really this documentation should be updated when any checker is changed related to errno modeling (errno modeling can be added later to any checker that evaluates standard functions, for example StreamChecker). Is it required to mention the ErrnoModeling dependency? (The modeling checker is turned on always?) Or add documentation for ErrnoModeling too?

clang/test/Analysis/errno-stdlibraryfunctions-notes.c

15–23 ↗

(On Diff #435558)

The CERT rule says that there is no guarantee that errno is not changed if the function is successful, regardless if it was 0 or not. There are some functions (that have in-band return value) where it is required to set errno to 0, there can be another checker (or extend ErrnoChecker) to check this.

The new warning is turned on when alpha.unix.Errno is turned on, otherwise it should not appear.

[martong]

clang/test/Analysis/errno-stdlibraryfunctions-notes.c

15–23 ↗

(On Diff #435558)

I must say that I dislike that one cannot disable this warning unless they disable the whole stdlibrarymodeling.

Yeah, good point. Perhaps we should have a new checker option that enables/disables errno related reports. Should this be part of the ErrnoChecker (or the StdLibraryFunctionsChecker)?

[steakhal]

It looks everything fine, given that the alpha.unix.Errno will depend on the apimodeling.StdCLibraryFunctions.
This should do the expected errno state propagation by which the Errno checker can report diagnostics - WHILE the StdCLibraryFunctions still won't report diagnostics.
This means that the Errno part /diagnostics can be separately disabled from the diagnostics of StdCLibraryFunctionArgsChecker and other frontend checkers of the StdCLibraryFunctionsChecker modeling part.
Excellent.

Please demonstrate that indeed disabling separately Errno or StdCLibraryFunctionArgsChecker will make the respective reports disappear.

---

I can see that in many cases you introduced an additional .Case(), which will result in a state-split.
I'm curious what runtime implications this change introduces. Please measure this.

I must also admit that I haven't checked the parameters of Case() in all cases; so I would encourage you to double-check those to make sure they are in line with the API specification.

Given these changes are implemented, I think it's ready to land. Awesome job, really!
Sorry about reject, I just saw it's green and I still had some thoughts about this.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

68–69

446

nit: we should not use the NN and other suffixed versions of this API. The generic one should suffice.
Actually, I plan to refactor all code and make those private.

clang/test/Analysis/errno-stdlibraryfunctions-notes.c

15–23 ↗

(On Diff #435558)

The new warning is turned on when alpha.unix.Errno is turned on, otherwise it should not appear.

Oh, I see. I might overreacted this part.

[steakhal]

In the describeErrnoCheckState() the Errno_MustBeChecked is uncovered by tests.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

412

I would prefer the west-const style.

[balazske]

Small fixes.

[steakhal]

LGTM, good job.

[balazske]

I did performance measurements in the past and it showed no important difference, run time got more with at most some percent at some of the projects.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

 // because if the function has no other effects, other checkers would probably
 // never want to improve upon the modeling done by this checker.
 //
 // Non-pure functions, for which only partial improvement over the default
 // behavior is expected, are modeled via check::PostCall, non-intrusively.
 //
 //===----------------------------------------------------------------------===//
 
+#include "ErrnoModeling.h"
 #include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/DynamicExtent.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/StringExtras.h"
 
 #include <string>
 
 using namespace clang;
 using namespace clang::ento;
 
+static const char *describeErrnoCheckState(errno_modeling::ErrnoCheckState CS) {
+  switch (CS) {
+  case errno_modeling::Errno_Irrelevant:
+    return "is not significant";
+  case errno_modeling::Errno_MustBeChecked:
+    return "should be checked to verify if the call was successful";
+  case errno_modeling::Errno_MustNotBeChecked:
+    return "may be undefined after the call and should not be used";
+  default:
+    llvm_unreachable("unknown enum value");
+  };
+}
+
 namespace {
 class StdLibraryFunctionsChecker
     : public Checker<check::PreCall, check::PostCall, eval::Call> {
 
   class Summary;
 
   /// Specify how much the analyzer engine should entrust modeling this function
   /// to us. If he doesn't, he performs additional invalidations.
bool checkSpecificValidity(const FunctionDecl *FD) const override {
              "This constraint should be applied only on a pointer type");
       return ValidArg;
     }
   };
 
   /// The complete list of constraints that defines a single branch.
   using ConstraintSet = std::vector<ValueConstraintPtr>;
 
+  /// Define how a function affects the system variable 'errno'.
+  /// This works together with the ErrnoModeling and ErrnoChecker classes.
+  class ErrnoConstraintBase {
+  public:
+    /// Apply specific state changes related to the errno variable.
+    virtual ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
+                                  const Summary &Summary,
+                                  CheckerContext &C) const = 0;
+    /// Get a description about what is applied to 'errno' and how is it allowed
+    /// to be used. If ErrnoChecker generates a bug then this message is
+    /// displayed as a note at the function call.
+    /// It may return empty string if no note tag is to be added.
+    virtual std::string describe(StringRef FunctionName) const { return ""; }
+
+    virtual ~ErrnoConstraintBase() {}
+
+  protected:
+    /// Many of the descendant classes use this value.
+    errno_modeling::ErrnoCheckState const CheckState;
+
+    ErrnoConstraintBase(errno_modeling::ErrnoCheckState CS) : CheckState(CS) {}
+
+    /// This is used for conjure symbol for errno to differentiate from the
+    /// original call expression (same expression is used for the errno symbol).
+    static int Tag;
+  };
+
+  /// Set value of 'errno' to be related to 0 in a specified way, with a
+  /// specified "errno check state". For example with \c BO_GT 'errno' is
+  /// constrained to be greater than 0. Use this for failure cases of functions.
+  class ZeroRelatedErrnoConstraint : public ErrnoConstraintBase {
+    BinaryOperatorKind Op;
+
+  public:
+    ZeroRelatedErrnoConstraint(clang::BinaryOperatorKind OpK,
+                               errno_modeling::ErrnoCheckState CS)
+        : ErrnoConstraintBase(CS), Op(OpK) {
+      assert(BinaryOperator::isRelationalOp(OpK));
+    }
+
+    ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
+                          const Summary &Summary,
+                          CheckerContext &C) const override {
+      SValBuilder &SVB = C.getSValBuilder();
+      NonLoc ErrnoSVal =
+          SVB.conjureSymbolVal(&Tag, Call.getOriginExpr(),
+                               C.getLocationContext(), C.getASTContext().IntTy,
+                               C.blockCount())
+              .castAs<NonLoc>();
+      NonLoc ZeroVal =
+          SVB.makeZeroVal(C.getASTContext().IntTy).castAs<NonLoc>();
+      DefinedOrUnknownSVal Cond =
+          SVB.evalBinOpNN(State, Op, ErrnoSVal, ZeroVal, SVB.getConditionType())
+              .castAs<DefinedOrUnknownSVal>();
+      State = State->assume(Cond, true);
+      if (!State)
+        return State;
+      return errno_modeling::setErrnoValue(State, C.getLocationContext(),
+                                           ErrnoSVal, CheckState);
+    }
+
+    std::string describe(StringRef FunctionName) const override {
+      Twine Result = "Assuming that function '";
+      Result.concat(FunctionName.str());
+      Result.concat("' fails, in this case the value 'errno' becomes ");
+      Result.concat(BinaryOperator::getOpcodeStr(Op).str());
+      Result.concat(" 0 and ");
+      Result.concat(describeErrnoCheckState(CheckState));
+      return Result.str();
+    }
+  };
+
+  /// Applies the constraints to 'errno' for a common case when a standard
+  /// function is successful. The value of 'errno' after the call is not
+  /// specified by the standard (it may change or not). The \c ErrnoChecker can
+  /// generate a bug if 'errno' is read afterwards.
+  class SuccessErrnoConstraint : public ErrnoConstraintBase {
+  public:
+    SuccessErrnoConstraint()
+        : ErrnoConstraintBase(errno_modeling::Errno_MustNotBeChecked) {}
+
+    ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
+                          const Summary &Summary,
+                          CheckerContext &C) const override {
+      return errno_modeling::setErrnoState(State, CheckState);
+    }
+
+    std::string describe(StringRef FunctionName) const override {
+      Twine Result = "Assuming that function '";
+      Result.concat(FunctionName.str());
+      Result.concat("' is successful, in this case the value 'errno' ");
+      Result.concat(describeErrnoCheckState(CheckState));
+      return Result.str();
+    }
+  };
+
+  /// Set errno constraints if use of 'errno' is completely irrelevant to the
+  /// modeled function or modeling is not possible.
+  class NoErrnoConstraint : public ErrnoConstraintBase {
+  public:
+    NoErrnoConstraint()
+        : ErrnoConstraintBase(errno_modeling::Errno_Irrelevant) {}
+
+    ProgramStateRef apply(ProgramStateRef State, const CallEvent &Call,
+                          const Summary &Summary,
+                          CheckerContext &C) const override {
+      return errno_modeling::setErrnoState(State, CheckState);
+    }
+  };
+
   /// A single branch of a function summary.
   ///
   /// A branch is defined by a series of constraints - "assumptions" -
   /// that together form a single possible outcome of invoking the function.
   /// When static analyzer considers a branch, it tries to introduce
   /// a child node in the Exploded Graph. The child node has to include
   /// constraints that define the branch. If the constraints contradict
   /// existing constraints in the state, the node is not created and the branch
   /// is dropped; otherwise it's queued for future exploration.
   /// The branch is accompanied by a note text that may be displayed
   /// to the user when a bug is found on a path that takes this branch.
   ///
   /// For example, consider the branches in `isalpha(x)`:
   ///   Branch 1)
   ///     x is in range ['A', 'Z'] or in ['a', 'z']
   ///     then the return value is not 0. (I.e. out-of-range [0, 0])
   ///     and the note may say "Assuming the character is alphabetical"
   ///   Branch 2)
   ///     x is out-of-range ['A', 'Z'] and out-of-range ['a', 'z']
   ///     then the return value is 0
   ///     and the note may say "Assuming the character is non-alphabetical".
   class SummaryCase {
     ConstraintSet Constraints;
+    const ErrnoConstraintBase &ErrnoConstraint;
     StringRef Note;
 
   public:
-    SummaryCase(ConstraintSet &&Constraints, StringRef Note)
-        : Constraints(std::move(Constraints)), Note(Note) {}
-
-    SummaryCase(const ConstraintSet &Constraints, StringRef Note)
-        : Constraints(Constraints), Note(Note) {}
+    SummaryCase(ConstraintSet &&Constraints, const ErrnoConstraintBase &ErrnoC,
+                StringRef Note)
+        : Constraints(std::move(Constraints)), ErrnoConstraint(ErrnoC),
+          Note(Note) {}
+
+    SummaryCase(const ConstraintSet &Constraints,
+                const ErrnoConstraintBase &ErrnoC, StringRef Note)
+        : Constraints(Constraints), ErrnoConstraint(ErrnoC), Note(Note) {}
 
     const ConstraintSet &getConstraints() const { return Constraints; }
+    const ErrnoConstraintBase &getErrnoConstraint() const {
+      return ErrnoConstraint;
+    }
     StringRef getNote() const { return Note; }
   };
 
   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.
class Summary {
 
     // The function to which the summary applies. This is set after lookup and
     // match to the signature.
     const FunctionDecl *FD = nullptr;
 
   public:
     Summary(InvalidationKind InvalidationKd) : InvalidationKd(InvalidationKd) {}
 
-    Summary &Case(ConstraintSet &&CS, StringRef Note = "") {
-      Cases.push_back(SummaryCase(std::move(CS), Note));
+    Summary &Case(ConstraintSet &&CS, const ErrnoConstraintBase &ErrnoC,
+                  StringRef Note = "") {
+      Cases.push_back(SummaryCase(std::move(CS), ErrnoC, Note));
       return *this;
     }
-    Summary &Case(const ConstraintSet &CS, StringRef Note = "") {
-      Cases.push_back(SummaryCase(CS, Note));
+    Summary &Case(const ConstraintSet &CS, const ErrnoConstraintBase &ErrnoC,
+                  StringRef Note = "") {
+      Cases.push_back(SummaryCase(CS, ErrnoC, Note));
       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;
     }
void reportBug(const CallEvent &Call, ExplodedNode *N,
     R->addRange(Call.getArgSourceRange(VC->getArgNo()));
 
     // Describe the argument constraint in a note.
     R->addNote(VC->describe(C.getState(), Summary), R->getLocation(),
                Call.getArgSourceRange(VC->getArgNo()));
 
     C.emitReport(std::move(R));
   }
+
+  /// These are the errno constraints that can be passed to summary cases.
+  /// One of these should fit for a single summary case.
+  /// Usually if a failure return value exists for function, that function
+  /// needs different cases for success and failure with different errno
+  /// constraints (and different return value constraints).
+  const NoErrnoConstraint ErrnoIrrelevant;
+  const SuccessErrnoConstraint ErrnoMustNotBeChecked;
+  const ZeroRelatedErrnoConstraint ErrnoNEZeroIrrelevant{
+      clang::BinaryOperatorKind::BO_NE, errno_modeling::Errno_Irrelevant};
 };
 
+int StdLibraryFunctionsChecker::ErrnoConstraintBase::Tag = 0;
+
 const StdLibraryFunctionsChecker::ArgNo StdLibraryFunctionsChecker::Ret =
     std::numeric_limits<ArgNo>::max();
 
 } // end of anonymous namespace
 
 static BasicValueFactory &getBVF(ProgramStateRef State) {
   ProgramStateManager &Mgr = State->getStateManager();
   SValBuilder &SVB = Mgr.getSValBuilder();
void StdLibraryFunctionsChecker::checkPostCall(const CallEvent &Call,
   for (const SummaryCase &Case : Summary.getCases()) {
     ProgramStateRef NewState = State;
     for (const ValueConstraintPtr &Constraint : Case.getConstraints()) {
       NewState = Constraint->apply(NewState, Call, Summary, C);
       if (!NewState)
         break;
     }
 
+    if (NewState)
+      NewState = Case.getErrnoConstraint().apply(NewState, Call, Summary, C);
+
     if (NewState && NewState != State) {
+      if (Case.getNote().empty()) {
+        std::string Note;
+        if (const auto *D = dyn_cast_or_null<FunctionDecl>(Call.getDecl()))
+          Note = Case.getErrnoConstraint().describe(D->getNameAsString());
+        if (Note.empty())
+          C.addTransition(NewState);
+        else
+          C.addTransition(NewState, errno_modeling::getErrnoNoteTag(C, Note));
+      } else {
         StringRef Note = Case.getNote();
         const NoteTag *Tag = C.getNoteTag(
             // Sorry couldn't help myself.
-          [Node, Note]() {
+            [Node, Note]() -> std::string {
               // Don't emit "Assuming..." note when we ended up
               // knowing in advance which branch is taken.
               return (Node->succ_size() > 1) ? Note.str() : "";
             },
             /*IsPrunable=*/true);
         C.addTransition(NewState, Tag);
       }
     }
   }
+}
 
 bool StdLibraryFunctionsChecker::evalCall(const CallEvent &Call,
                                           CheckerContext &C) const {
   Optional<Summary> FoundSummary = findFunctionSummary(Call, C);
   if (!FoundSummary)
     return false;
 
   const Summary &Summary = *FoundSummary;
   switch (Summary.getInvalidationKd()) {
   case EvalCallAsPure: {
     ProgramStateRef State = C.getState();
     const LocationContext *LC = C.getLocationContext();
     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);
+
     C.addTransition(State);
+
     return true;
   }
   case NoEvalCall:
     // Summary tells us to avoid performing eval::Call. The function is possibly
     // evaluated by another checker, or evaluated conservatively.
     return false;
   }
   llvm_unreachable("Unknown invalidation kind!");
void StdLibraryFunctionsChecker::initFunctionSummaries(
   // 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))},
-                "Assuming the character is alphanumeric")
+                ErrnoIrrelevant, "Assuming the character is alphanumeric")
           // 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, WithinRange, {{128, UCharRangeMax}})},
+                ErrnoIrrelevant)
           .Case(
               {ArgumentCondition(
                    0U, OutOfRange,
                    {{'0', '9'}, {'A', 'Z'}, {'a', 'z'}, {128, UCharRangeMax}}),
                ReturnValueCondition(WithinRange, SingleValue(0))},
-              "Assuming the character is non-alphanumeric")
+              ErrnoIrrelevant, "Assuming the character is non-alphanumeric")
           .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))},
-                "Assuming the character is alphabetical")
+                ErrnoIrrelevant, "Assuming the character is alphabetical")
           // The locale-specific range.
-          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
+          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})},
+                ErrnoIrrelevant)
           .Case({ArgumentCondition(
                      0U, OutOfRange,
                      {{'A', 'Z'}, {'a', 'z'}, {128, UCharRangeMax}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
-                "Assuming the character is non-alphabetical"));
+                ErrnoIrrelevant, "Assuming the character is non-alphabetical"));
   addToFunctionSummaryMap(
       "isascii", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range(0, 127)),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
-                "Assuming the character is an ASCII character")
+                ErrnoIrrelevant, "Assuming the character is an ASCII character")
           .Case({ArgumentCondition(0U, OutOfRange, Range(0, 127)),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not an ASCII character"));
   addToFunctionSummaryMap(
       "isblank", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, {{'\t', '\t'}, {' ', ' '}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
-                "Assuming the character is a blank character")
+                ErrnoIrrelevant, "Assuming the character is a blank character")
           .Case({ArgumentCondition(0U, OutOfRange, {{'\t', '\t'}, {' ', ' '}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not a blank character"));
   addToFunctionSummaryMap(
       "iscntrl", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, {{0, 32}, {127, 127}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is a control character")
           .Case({ArgumentCondition(0U, OutOfRange, {{0, 32}, {127, 127}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not a control character"));
   addToFunctionSummaryMap(
       "isdigit", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range('0', '9')),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
-                "Assuming the character is a digit")
+                ErrnoIrrelevant, "Assuming the character is a digit")
           .Case({ArgumentCondition(0U, OutOfRange, Range('0', '9')),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
-                "Assuming the character is not a digit"));
+                ErrnoIrrelevant, "Assuming the character is not a digit"));
   addToFunctionSummaryMap(
       "isgraph", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range(33, 126)),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character has graphical representation")
           .Case(
               {ArgumentCondition(0U, OutOfRange, Range(33, 126)),
                ReturnValueCondition(WithinRange, SingleValue(0))},
+              ErrnoIrrelevant,
               "Assuming the character does not have graphical representation"));
   addToFunctionSummaryMap(
       "islower", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           // Is certainly lowercase.
           .Case({ArgumentCondition(0U, WithinRange, Range('a', 'z')),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
-                "Assuming the character is a lowercase letter")
+                ErrnoIrrelevant, "Assuming the character is a lowercase letter")
           // Is ascii but not lowercase.
           .Case({ArgumentCondition(0U, WithinRange, Range(0, 127)),
                  ArgumentCondition(0U, OutOfRange, Range('a', 'z')),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not a lowercase letter")
           // The locale-specific range.
-          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
+          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})},
+                ErrnoIrrelevant)
           // Is not an unsigned char.
           .Case({ArgumentCondition(0U, OutOfRange, Range(0, UCharRangeMax)),
-                 ReturnValueCondition(WithinRange, SingleValue(0))}));
+                 ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant));
   addToFunctionSummaryMap(
       "isprint", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange, Range(32, 126)),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
-                "Assuming the character is printable")
+                ErrnoIrrelevant, "Assuming the character is printable")
           .Case({ArgumentCondition(0U, OutOfRange, Range(32, 126)),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
-                "Assuming the character is non-printable"));
+                ErrnoIrrelevant, "Assuming the character is non-printable"));
   addToFunctionSummaryMap(
       "ispunct", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(
                      0U, WithinRange,
                      {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
-                "Assuming the character is a punctuation mark")
+                ErrnoIrrelevant, "Assuming the character is a punctuation mark")
           .Case({ArgumentCondition(
                      0U, OutOfRange,
                      {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not a punctuation mark"));
   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))},
+                ErrnoIrrelevant,
                 "Assuming the character is a whitespace character")
           // The locale-specific range.
-          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
+          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})},
+                ErrnoIrrelevant)
           .Case({ArgumentCondition(0U, OutOfRange,
                                    {{9, 13}, {' ', ' '}, {128, UCharRangeMax}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not a whitespace character"));
   addToFunctionSummaryMap(
       "isupper", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           // Is certainly uppercase.
           .Case({ArgumentCondition(0U, WithinRange, Range('A', 'Z')),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is an uppercase letter")
           // The locale-specific range.
-          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})})
+          .Case({ArgumentCondition(0U, WithinRange, {{128, UCharRangeMax}})},
+                ErrnoIrrelevant)
           // Other.
           .Case({ArgumentCondition(0U, OutOfRange,
                                    {{'A', 'Z'}, {128, UCharRangeMax}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not an uppercase letter"));
   addToFunctionSummaryMap(
       "isxdigit", Signature(ArgTypes{IntTy}, RetType{IntTy}),
       Summary(EvalCallAsPure)
           .Case({ArgumentCondition(0U, WithinRange,
                                    {{'0', '9'}, {'A', 'F'}, {'a', 'f'}}),
                  ReturnValueCondition(OutOfRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is a hexadecimal digit")
           .Case({ArgumentCondition(0U, OutOfRange,
                                    {{'0', '9'}, {'A', 'F'}, {'a', 'f'}}),
                  ReturnValueCondition(WithinRange, SingleValue(0))},
+                ErrnoIrrelevant,
                 "Assuming the character is not a hexadecimal digit"));
   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}})}));
+                                      {{EOFv, EOFv}, {0, UCharRangeMax}})},
+                ErrnoIrrelevant));
   addToFunctionSummaryMap(
       "getchar", Signature(ArgTypes{}, RetType{IntTy}),
       Summary(NoEvalCall)
           .Case({ReturnValueCondition(WithinRange,
-                                      {{EOFv, EOFv}, {0, UCharRangeMax}})}));
+                                      {{EOFv, EOFv}, {0, UCharRangeMax}})},
+                ErrnoIrrelevant));
 
   // read()-like functions that never return more than buffer size.
   auto FreadSummary =
       Summary(NoEvalCall)
           .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-                 ReturnValueCondition(WithinRange, Range(0, SizeMax))})
+                 ReturnValueCondition(WithinRange, Range(0, SizeMax))},
+                ErrnoIrrelevant)
           .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(
addToFunctionSummaryMap("fwrite",
                           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))});
+                 ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))},
+                ErrnoIrrelevant);
 
   // 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}))});
+                                      Range({-1, -1}, {1, Ssize_tMax}))},
+                ErrnoIrrelevant);
 
   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(
                          FilePtrRestrictTy},
                 RetType{Ssize_tTy}),
       GetLineSummary);
 
   {
     Summary GetenvSummary =
         Summary(NoEvalCall)
             .ArgConstraint(NotNull(ArgNo(0)))
-            .Case({NotNull(Ret)}, "Assuming the environment variable exists");
+            .Case({NotNull(Ret)}, ErrnoIrrelevant,
+                  "Assuming the environment variable exists");
     // In untrusted environments the envvar might not exist.
     if (!ShouldAssumeControlledEnvironment)
-      GetenvSummary.Case({NotNull(Ret)->negate()},
+      GetenvSummary.Case({NotNull(Ret)->negate()}, ErrnoIrrelevant,
                          "Assuming the environment variable does not exist");
 
     // 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 ReturnsZero =
+        ConstraintSet{ReturnValueCondition(WithinRange, SingleValue(0))};
+    const auto ReturnsMinusOne =
+        ConstraintSet{ReturnValueCondition(WithinRange, SingleValue(-1))};
+    const auto ReturnsNonnegative =
+        ConstraintSet{ReturnValueCondition(WithinRange, Range(0, IntMax))};
     const auto ReturnsFileDescriptor =
         ConstraintSet{ReturnValueCondition(WithinRange, Range(-1, IntMax))};
+    const auto &ReturnsValidFileDescriptor = ReturnsNonnegative;
 
     // int access(const char *pathname, int amode);
     addToFunctionSummaryMap(
         "access", Signature(ArgTypes{ConstCharPtrTy, IntTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))));
+    addToFunctionSummaryMap(
+        "dup", Signature(ArgTypes{IntTy}, RetType{IntTy}),
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
+            .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)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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)
+        Summary(NoEvalCall)
             .ArgConstraint(NotNull(ArgNo(0)))
             .ArgConstraint(NotNull(ArgNo(1))));
 
     // int fsync(int fildes);
     addToFunctionSummaryMap("fsync", Signature(ArgTypes{IntTy}, RetType{IntTy}),
                             Summary(NoEvalCall)
-                                .Case(ReturnsZeroOrMinusOne)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(NotNull(ArgNo(0))));
 
     // int symlink(const char *oldpath, const char *newpath);
     addToFunctionSummaryMap(
         "symlink",
         Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))));
+    addToFunctionSummaryMap(
+        "dirfd", Signature(ArgTypes{DirPtrTy}, RetType{IntTy}),
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
 
     // 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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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))));
+    addToFunctionSummaryMap(
+        "mkstemp", Signature(ArgTypes{CharPtrTy}, RetType{IntTy}),
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
 
     // char *mkdtemp(char *template);
+    // FIXME: Improve for errno modeling.
     addToFunctionSummaryMap(
         "mkdtemp", Signature(ArgTypes{CharPtrTy}, RetType{CharPtrTy}),
         Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // char *getcwd(char *buf, size_t size);
+    // FIXME: Improve for errno modeling.
     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);
+    // FIXME: returns 0 on success, ReturnsValidFileDescriptor is incorrect
     addToFunctionSummaryMap(
         "mkdir", Signature(ArgTypes{ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(NotNull(ArgNo(0))));
 
     // int mkdirat(int dirfd, const char *pathname, mode_t mode);
+    // FIXME: returns 0 on success, ReturnsValidFileDescriptor is incorrect
     addToFunctionSummaryMap(
         "mkdirat",
         Signature(ArgTypes{IntTy, ConstCharPtrTy, Mode_tTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(NotNull(ArgNo(1))));
 
     Optional<QualType> Dev_tTy = lookupTy("dev_t");
 
     // int mknod(const char *pathname, mode_t mode, dev_t dev);
+    // FIXME: returns 0 on success, ReturnsValidFileDescriptor is incorrect
     addToFunctionSummaryMap(
         "mknod",
         Signature(ArgTypes{ConstCharPtrTy, Mode_tTy, Dev_tTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(NotNull(ArgNo(0))));
 
     // int mknodat(int dirfd, const char *pathname, mode_t mode, dev_t dev);
+    // FIXME: returns 0 on success, ReturnsValidFileDescriptor is incorrect
     addToFunctionSummaryMap(
         "mknodat",
         Signature(ArgTypes{IntTy, ConstCharPtrTy, Mode_tTy, Dev_tTy},
                   RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(
                 ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
     // int rmdir(const char *pathname);
     addToFunctionSummaryMap("rmdir",
                             Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
                             Summary(NoEvalCall)
-                                .Case(ReturnsZeroOrMinusOne)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .ArgConstraint(NotNull(ArgNo(0))));
 
     // int chdir(const char *path);
     addToFunctionSummaryMap("chdir",
                             Signature(ArgTypes{ConstCharPtrTy}, RetType{IntTy}),
                             Summary(NoEvalCall)
-                                .Case(ReturnsZeroOrMinusOne)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .ArgConstraint(NotNull(ArgNo(0))));
 
     // int link(const char *oldpath, const char *newpath);
     addToFunctionSummaryMap(
         "link",
         Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(ArgumentCondition(0, WithinRange, Range(0, IntMax)))
             .ArgConstraint(NotNull(ArgNo(1)))
             .ArgConstraint(NotNull(ArgNo(2))));
 
     // DIR *opendir(const char *name);
+    // FIXME: Improve for errno modeling.
     addToFunctionSummaryMap(
         "opendir", Signature(ArgTypes{ConstCharPtrTy}, RetType{DirPtrTy}),
         Summary(NoEvalCall).ArgConstraint(NotNull(ArgNo(0))));
 
     // DIR *fdopendir(int fd);
+    // FIXME: Improve for errno modeling.
     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))})
+            .Case({ReturnValueCondition(WithinRange, Range(0, 1))},
+                  ErrnoIrrelevant)
             .ArgConstraint(
                 ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
     // FILE *popen(const char *command, const char *type);
+    // FIXME: Improve for errno modeling.
     addToFunctionSummaryMap(
         "popen",
         Signature(ArgTypes{ConstCharPtrTy, ConstCharPtrTy}, RetType{FilePtrTy}),
         Summary(NoEvalCall)
             .ArgConstraint(NotNull(ArgNo(0)))
             .ArgConstraint(NotNull(ArgNo(1))));
 
     // int pclose(FILE *stream);
+    // FIXME: Improve for errno modeling.
     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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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);
+    // FIXME: Improve for errno modeling.
     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))));
+    addToFunctionSummaryMap(
+        "fileno", Signature(ArgTypes{FilePtrTy}, RetType{IntTy}),
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
 
     // int fseeko(FILE *stream, off_t offset, int whence);
     addToFunctionSummaryMap(
         "fseeko",
         Signature(ArgTypes{FilePtrTy, Off_tTy, IntTy}, RetType{IntTy}),
         Summary(NoEvalCall)
-            .Case(ReturnsZeroOrMinusOne)
+            .Case(ReturnsZeroOrMinusOne, ErrnoIrrelevant)
             .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);
+    // FIXME: Improve for errno modeling.
     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);
+    // FIXME: Improve for errno modeling.
     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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .ArgConstraint(NotNull(ArgNo(0))));
 
     // off_t lseek(int fildes, off_t offset, int whence);
+    // In the first case we can not tell for sure if it failed or not.
+    // A return value different from of the expected offset (that is unknown
+    // here) may indicate failure. For this reason we do not enforce the errno
+    // check (can cause false positive).
     addToFunctionSummaryMap(
         "lseek", Signature(ArgTypes{IntTy, Off_tTy, IntTy}, RetType{Off_tTy}),
         Summary(NoEvalCall)
+            .Case(ReturnsNonnegative, ErrnoIrrelevant)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))})
+                   ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))})
+                   ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .ArgConstraint(NotNull(ArgNo(1)))
             .ArgConstraint(NotNull(ArgNo(3))));
 
     // char *realpath(const char *restrict file_name,
     //                char *restrict resolved_name);
+    // FIXME: Improve for errno modeling.
     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))})
+            .Case({ReturnValueCondition(WithinRange, SingleValue(-1))},
+                  ErrnoIrrelevant)
             .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))})
+            .Case({ReturnValueCondition(WithinRange, SingleValue(-1))},
+                  ErrnoIrrelevant)
             .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))})
+            .Case({ReturnValueCondition(WithinRange, Range(-1, UCharRangeMax))},
+                  ErrnoIrrelevant)
             .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));
if (ModelPOSIX) {
     // 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)
+            .Case(ReturnsValidFileDescriptor, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                 .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)
+              .Case(ReturnsZero, ErrnoMustNotBeChecked)
+              .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
               .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)
+                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                 .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)
+              .Case(ReturnsZero, ErrnoMustNotBeChecked)
+              .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
               .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)
+                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                 .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)
+              .Case(ReturnsZero, ErrnoMustNotBeChecked)
+              .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
               .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)
+                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                 .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)
+              .Case(ReturnsZero, ErrnoMustNotBeChecked)
+              .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
               .ArgConstraint(
                   ArgumentCondition(0, WithinRange, Range(0, IntMax))));
 
     auto Recvfrom =
         Summary(NoEvalCall)
             .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-                   ReturnValueCondition(WithinRange, Range(-1, Ssize_tMax))})
+                   ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))})
+                   ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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))})
+                   ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))})
+            .Case({ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))})
+            .Case({ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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))})
+                   ReturnValueCondition(WithinRange, Range(0, Ssize_tMax))},
+                  ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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
if (ModelPOSIX) {
     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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+                                .Case(ReturnsZero, ErrnoMustNotBeChecked)
+                                .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
                                 .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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> 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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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)
+            .Case(ReturnsZero, ErrnoMustNotBeChecked)
+            .Case(ReturnsMinusOne, ErrnoNEZeroIrrelevant)
             .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");

clang/test/Analysis/Inputs/system-header-simulator-for-errno.h

+#pragma clang system_header
+
+typedef __typeof(sizeof(int)) off_t;
+
+int access(const char *path, int amode);
+off_t lseek(int fildes, off_t offset, int whence);

clang/test/Analysis/errno-stdlibraryfunctions.c

+// RUN: %clang_analyze_cc1 -verify -analyzer-output text %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=apiModeling.StdCLibraryFunctions \
+// RUN:   -analyzer-checker=apiModeling.Errno \
+// RUN:   -analyzer-checker=alpha.unix.Errno \
+// RUN:   -analyzer-config apiModeling.StdCLibraryFunctions:ModelPOSIX=true
+
+#include "Inputs/errno_var.h"
+#include "Inputs/system-header-simulator-for-errno.h"
+
+void test1() {
+  access("path", 0); // no note here
+  access("path", 0);
+  // expected-note@-1{{Assuming that function 'access' is successful, in this case the value 'errno' may be undefined after the call and should not be used}}
+  if (errno != 0) { }
+  // expected-warning@-1{{An undefined value may be read from 'errno'}}
+  // expected-note@-2{{An undefined value may be read from 'errno'}}
+}
+
+void test2() {
+  if (access("path", 0) == -1) {
+    if (errno != 0) { }
+  }
+}
+
+void test3() {
+  if (access("path", 0) != -1) {
+    // expected-note@-1{{Assuming that function 'access' is successful, in this case the value 'errno' may be undefined after the call and should not be used}}
+    if (errno != 0) { }
+    // expected-warning@-1{{An undefined value may be read from 'errno'}}
+    // expected-note@-2{{An undefined value may be read from 'errno'}}
+  }
+}