diff --git a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp --- a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp @@ -160,15 +160,29 @@ /// The complete list of ranges that defines a single branch. typedef std::vector ValueRangeSet; + using ArgTypesTy = std::vector; + using RetTypeTy = QualType; + using RangesTy = std::vector; + /// Includes information about function prototype (which is necessary to /// ensure we're modeling the right function and casting values properly), /// approach to invalidation, and a list of branches - essentially, a list /// of list of ranges - essentially, a list of lists of lists of segments. struct FunctionSummaryTy { - const std::vector ArgTypes; - const QualType RetType; + const ArgTypesTy ArgTypes; + const RetTypeTy RetType; const InvalidationKindTy InvalidationKind; - const std::vector Ranges; + RangesTy Ranges; + + FunctionSummaryTy(ArgTypesTy ArgTypes, RetTypeTy RetType, + InvalidationKindTy InvalidationKind) + : ArgTypes(ArgTypes), RetType(RetType), + InvalidationKind(InvalidationKind) {} + + FunctionSummaryTy &Specification(ValueRangeSet VRS) { + Ranges.push_back(VRS); + return *this; + } private: static void assertTypeSuitableForSummary(QualType T) { @@ -517,538 +531,286 @@ // // Please update the list of functions in the header after editing! // - // The format is as follows: + + // Below are helper functions to create the summaries. // + // The format is as follows: //{ "function name", - // { spec: + // { variant0: // { argument types list, ... }, - // return type, purity, { range set list: + // return type, purity, { specification list: // { range list: // { argument index, within or out of, {{from, to}, ...} }, // { argument index, compares to argument, {{how, which}} }, // ... // } // } + // }, + // { variant1: + // ... // } //} + using Summary = FunctionSummaryTy; + auto ArgumentCondition = [](ArgNoTy ArgNo, ValueRangeKindTy Kind, + IntRangeVectorTy Ranges) -> ValueRange { + ValueRange VR{ArgNo, Kind, Ranges}; + return VR; + }; + auto ReturnValueCondition = [](ValueRangeKindTy Kind, + IntRangeVectorTy Ranges) -> ValueRange { + ValueRange VR{Ret, Kind, Ranges}; + return VR; + }; + auto Range = [](RangeIntTy b, RangeIntTy e) { + return IntRangeVectorTy{std::pair{b, e}}; + }; + auto SingleValue = [](RangeIntTy v) { + return IntRangeVectorTy{std::pair{v, v}}; + }; + auto IsLessThan = [](ArgNoTy ArgNo) { + return IntRangeVectorTy{{BO_LE, ArgNo}}; + }; -#define SUMMARY_WITH_VARIANTS(identifier) {#identifier, { -#define END_SUMMARY_WITH_VARIANTS }}, -#define VARIANT(argument_types, return_type, invalidation_approach) \ - { argument_types, return_type, invalidation_approach, { -#define END_VARIANT } }, -#define SUMMARY(identifier, argument_types, return_type, \ - invalidation_approach) \ - { #identifier, { { argument_types, return_type, invalidation_approach, { -#define END_SUMMARY } } } }, -#define ARGUMENT_TYPES(...) { __VA_ARGS__ } -#define RETURN_TYPE(x) x -#define INVALIDATION_APPROACH(x) x -#define CASE { -#define END_CASE }, -#define ARGUMENT_CONDITION(argument_number, condition_kind) \ - { argument_number, condition_kind, { -#define END_ARGUMENT_CONDITION }}, -#define RETURN_VALUE_CONDITION(condition_kind) \ - { Ret, condition_kind, { -#define END_RETURN_VALUE_CONDITION }}, -#define ARG_NO(x) x##U -#define RANGE(x, y) { x, y }, -#define SINGLE_VALUE(x) RANGE(x, x) -#define IS_LESS_THAN(arg) { BO_LE, arg } + // Templates for summaries that are reused by many functions. + auto GetcT = [&]() { + return Summary(ArgTypesTy{Irrelevant}, RetTypeTy(IntTy), NoEvalCall) + .Specification({ReturnValueCondition(WithinRange, Range(-1, 255))}); + }; + auto ReadT = [&](RetTypeTy R, RangeIntTy Max) { + return Summary(ArgTypesTy{Irrelevant, Irrelevant, SizeTy}, RetTypeTy(R), + NoEvalCall) + .Specification({ReturnValueCondition(ComparesToArgument, IsLessThan(2)), + ReturnValueCondition(WithinRange, Range(-1, Max))}); + }; + auto FreadT = [&]() { + return Summary(ArgTypesTy{Irrelevant, Irrelevant, SizeTy, Irrelevant}, + RetTypeTy(SizeTy), NoEvalCall) + .Specification({ + ReturnValueCondition(ComparesToArgument, IsLessThan(2)), + }); + }; + auto GetlineT = [&](RetTypeTy R, RangeIntTy Max) { + return Summary(ArgTypesTy{Irrelevant, Irrelevant, Irrelevant}, RetTypeTy(R), + NoEvalCall) + .Specification( + {ReturnValueCondition(WithinRange, {{-1, -1}, {1, Max}})}); + }; FunctionSummaryMap = { - // The isascii() family of functions. - SUMMARY(isalnum, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // Boils down to isupper() or islower() or isdigit() - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('0', '9') - RANGE('A', 'Z') - RANGE('a', 'z') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE // The locale-specific range. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(128, 255) - END_ARGUMENT_CONDITION - // No post-condition. We are completely unaware of - // locale-specific return values. - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('0', '9') - RANGE('A', 'Z') - RANGE('a', 'z') - RANGE(128, 255) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isalpha, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // isupper() or islower(). Note that 'Z' is less than 'a'. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('A', 'Z') - RANGE('a', 'z') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE // The locale-specific range. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(128, 255) - END_ARGUMENT_CONDITION - END_CASE - CASE // Other. - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('A', 'Z') - RANGE('a', 'z') - RANGE(128, 255) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isascii, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // Is ASCII. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(0, 127) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE(0, 127) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isblank, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - SINGLE_VALUE('\t') - SINGLE_VALUE(' ') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - SINGLE_VALUE('\t') - SINGLE_VALUE(' ') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(iscntrl, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // 0..31 or 127 - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(0, 32) - SINGLE_VALUE(127) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE(0, 32) - SINGLE_VALUE(127) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isdigit, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // Is a digit. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('0', '9') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('0', '9') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isgraph, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(33, 126) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE(33, 126) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(islower, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // Is certainly lowercase. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('a', 'z') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE // Is ascii but not lowercase. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(0, 127) - END_ARGUMENT_CONDITION - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('a', 'z') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE // The locale-specific range. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(128, 255) - END_ARGUMENT_CONDITION - END_CASE - CASE // Is not an unsigned char. - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE(0, 255) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isprint, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(32, 126) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE(32, 126) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(ispunct, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('!', '/') - RANGE(':', '@') - RANGE('[', '`') - RANGE('{', '~') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('!', '/') - RANGE(':', '@') - RANGE('[', '`') - RANGE('{', '~') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isspace, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // Space, '\f', '\n', '\r', '\t', '\v'. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(9, 13) - SINGLE_VALUE(' ') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE // The locale-specific range. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(128, 255) - END_ARGUMENT_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE(9, 13) - SINGLE_VALUE(' ') - RANGE(128, 255) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isupper, ARGUMENT_TYPES(IntTy), RETURN_TYPE (IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE // Is certainly uppercase. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('A', 'Z') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE // The locale-specific range. - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE(128, 255) - END_ARGUMENT_CONDITION - END_CASE - CASE // Other. - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('A', 'Z') RANGE(128, 255) - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(isxdigit, ARGUMENT_TYPES(IntTy), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(EvalCallAsPure)) - CASE - ARGUMENT_CONDITION(ARG_NO(0), WithinRange) - RANGE('0', '9') - RANGE('A', 'F') - RANGE('a', 'f') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(OutOfRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - CASE - ARGUMENT_CONDITION(ARG_NO(0), OutOfRange) - RANGE('0', '9') - RANGE('A', 'F') - RANGE('a', 'f') - END_ARGUMENT_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(0) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - - // The getc() family of functions that returns either a char or an EOF. - SUMMARY(getc, ARGUMENT_TYPES(Irrelevant), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(NoEvalCall)) - CASE // FIXME: EOF is assumed to be defined as -1. - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, 255) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(fgetc, ARGUMENT_TYPES(Irrelevant), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(NoEvalCall)) - CASE // FIXME: EOF is assumed to be defined as -1. - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, 255) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(getchar, ARGUMENT_TYPES(), RETURN_TYPE(IntTy), - INVALIDATION_APPROACH(NoEvalCall)) - CASE // FIXME: EOF is assumed to be defined as -1. - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, 255) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - - // read()-like functions that never return more than buffer size. - // We are not sure how ssize_t is defined on every platform, so we provide - // three variants that should cover common cases. - SUMMARY_WITH_VARIANTS(read) - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy), - RETURN_TYPE(IntTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, IntMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy), - RETURN_TYPE(LongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, LongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy), - RETURN_TYPE(LongLongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, LongLongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - END_SUMMARY_WITH_VARIANTS - SUMMARY_WITH_VARIANTS(write) - // Again, due to elusive nature of ssize_t, we have duplicate - // our summaries to cover different variants. - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy), - RETURN_TYPE(IntTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, IntMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy), - RETURN_TYPE(LongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, LongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy), - RETURN_TYPE(LongLongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - RETURN_VALUE_CONDITION(WithinRange) - RANGE(-1, LongLongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - END_SUMMARY_WITH_VARIANTS - SUMMARY(fread, - ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy, Irrelevant), - RETURN_TYPE(SizeTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - SUMMARY(fwrite, - ARGUMENT_TYPES(Irrelevant, Irrelevant, SizeTy, Irrelevant), - RETURN_TYPE(SizeTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(ComparesToArgument) - IS_LESS_THAN(ARG_NO(2)) - END_RETURN_VALUE_CONDITION - END_CASE - END_SUMMARY - - // getline()-like functions either fail or read at least the delimiter. - SUMMARY_WITH_VARIANTS(getline) - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, Irrelevant), - RETURN_TYPE(IntTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(-1) - RANGE(1, IntMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, Irrelevant), - RETURN_TYPE(LongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(-1) - RANGE(1, LongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, Irrelevant), - RETURN_TYPE(LongLongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(-1) - RANGE(1, LongLongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - END_SUMMARY_WITH_VARIANTS - SUMMARY_WITH_VARIANTS(getdelim) - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, Irrelevant, Irrelevant), - RETURN_TYPE(IntTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(-1) - RANGE(1, IntMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, Irrelevant, Irrelevant), - RETURN_TYPE(LongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(-1) - RANGE(1, LongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - VARIANT(ARGUMENT_TYPES(Irrelevant, Irrelevant, Irrelevant, Irrelevant), - RETURN_TYPE(LongLongTy), INVALIDATION_APPROACH(NoEvalCall)) - CASE - RETURN_VALUE_CONDITION(WithinRange) - SINGLE_VALUE(-1) - RANGE(1, LongLongMax) - END_RETURN_VALUE_CONDITION - END_CASE - END_VARIANT - END_SUMMARY_WITH_VARIANTS + // The isascii() family of functions. + { + "isalnum", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + // Boils down to isupper() or islower() or isdigit(). + .Specification( + {ArgumentCondition(0U, WithinRange, + {{'0', '9'}, {'A', 'Z'}, {'a', 'z'}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + // The locale-specific range. + // No post-condition. We are completely unaware of + // locale-specific return values. + .Specification( + {ArgumentCondition(0U, WithinRange, {{128, 255}})}) + .Specification( + {ArgumentCondition( + 0U, OutOfRange, + {{'0', '9'}, {'A', 'Z'}, {'a', 'z'}, {128, 255}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isalpha", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, + {{'A', 'Z'}, {'a', 'z'}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + // The locale-specific range. + .Specification( + {ArgumentCondition(0U, WithinRange, {{128, 255}})}) + .Specification( + {ArgumentCondition(0U, OutOfRange, + {{'A', 'Z'}, {'a', 'z'}, {128, 255}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isascii", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, Range(0, 127)), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, Range(0, 127)), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isblank", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, + {{'\t', '\t'}, {' ', ' '}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, + {{'\t', '\t'}, {' ', ' '}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "iscntrl", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, + {{0, 32}, {127, 127}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, {{0, 32}, {127, 127}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isdigit", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, Range('0', '9')), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, Range('0', '9')), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isgraph", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, Range(33, 126)), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, Range(33, 126)), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "islower", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + // Is certainly lowercase. + .Specification( + {ArgumentCondition(0U, WithinRange, Range('a', 'z')), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + // Is ascii but not lowercase. + .Specification( + {ArgumentCondition(0U, WithinRange, Range(0, 127)), + ArgumentCondition(0U, OutOfRange, Range('a', 'z')), + ReturnValueCondition(WithinRange, SingleValue(0))}) + // The locale-specific range. + .Specification( + {ArgumentCondition(0U, WithinRange, {{128, 255}})}) + // Is not an unsigned char. + .Specification( + {ArgumentCondition(0U, OutOfRange, Range(0, 255)), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isprint", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, Range(32, 126)), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, Range(32, 126)), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "ispunct", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition( + 0U, WithinRange, + {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition( + 0U, OutOfRange, + {{'!', '/'}, {':', '@'}, {'[', '`'}, {'{', '~'}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isspace", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + // Space, '\f', '\n', '\r', '\t', '\v'. + .Specification( + {ArgumentCondition(0U, WithinRange, + {{9, 13}, {' ', ' '}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + // The locale-specific range. + .Specification( + {ArgumentCondition(0U, WithinRange, {{128, 255}})}) + .Specification( + {ArgumentCondition(0U, OutOfRange, + {{9, 13}, {' ', ' '}, {128, 255}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isupper", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + // Is certainly uppercase. + .Specification( + {ArgumentCondition(0U, WithinRange, Range('A', 'Z')), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + // The locale-specific range. + .Specification( + {ArgumentCondition(0U, WithinRange, {{128, 255}})}) + // Other. + .Specification( + {ArgumentCondition(0U, OutOfRange, + {{'A', 'Z'}, {128, 255}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + { + "isxdigit", + FunctionVariantsTy{ + Summary(ArgTypesTy{IntTy}, RetTypeTy(IntTy), EvalCallAsPure) + .Specification( + {ArgumentCondition(0U, WithinRange, + {{'0', '9'}, {'A', 'F'}, {'a', 'f'}}), + ReturnValueCondition(OutOfRange, SingleValue(0))}) + .Specification( + {ArgumentCondition(0U, OutOfRange, + {{'0', '9'}, {'A', 'F'}, {'a', 'f'}}), + ReturnValueCondition(WithinRange, SingleValue(0))})}, + }, + + // The getc() family of functions that returns either a char or an EOF. + {"getc", FunctionVariantsTy{GetcT()}}, + {"fgetc", FunctionVariantsTy{GetcT()}}, + {"getchar", + FunctionVariantsTy{Summary(ArgTypesTy{}, RetTypeTy(IntTy), NoEvalCall) + .Specification({ReturnValueCondition( + WithinRange, Range(-1, 255))})}}, + + // read()-like functions that never return more than buffer size. + // We are not sure how ssize_t is defined on every platform, so we + // provide three variants that should cover common cases. + {"read", FunctionVariantsTy{ReadT(IntTy, IntMax), ReadT(LongTy, LongMax), + ReadT(LongLongTy, LongLongMax)}}, + {"write", FunctionVariantsTy{ReadT(IntTy, IntMax), ReadT(LongTy, LongMax), + ReadT(LongLongTy, LongLongMax)}}, + {"fread", FunctionVariantsTy{FreadT()}}, + {"fwrite", FunctionVariantsTy{FreadT()}}, + // getline()-like functions either fail or read at least the delimiter. + {"getline", + FunctionVariantsTy{GetlineT(IntTy, IntMax), GetlineT(LongTy, LongMax), + GetlineT(LongLongTy, LongLongMax)}}, + {"getdelim", + FunctionVariantsTy{GetlineT(IntTy, IntMax), GetlineT(LongTy, LongMax), + GetlineT(LongLongTy, LongLongMax)}}, }; }