Polyspace® Code Prover™ выполняет проверку Invalid Use of Standard Library Routine на стандартных библиотечных подпрограммах, чтобы определить, допустимы ли их аргументы. Проверка работает по-другому на стандартные программы памяти, стандартные программы с плавающей точкой или стандартные программы строки, потому что их аргументы могут быть недопустимыми по-разному. Эта тема описывает, как проверка работает на стандартную библиотеку стандартные программы с плавающей точкой.
Для получения дополнительной информации о проверке смотрите Invalid use of standard library routine.
Проверка Invalid Use of Standard Library Routine последовательно ищет следующие проблемы в использовании стандартных программ с плавающей точкой.
Доменная ошибка: доменная ошибка происходит, если аргументы функции недопустимы. Определение недействительного аргумента варьируется на основе того, позволяете ли вы неличные плавания или нет. Если вы позволяете неличные плавания, но:
Укажите, что вас нужно предупредить о результатах NaN, доменная ошибка происходит, если функция возвращает NaN, и самими аргументами не является NaN.
Укажите, что результаты NaN должны быть запрещены, доменная ошибка происходит, если функция возвращает NaN, или самими аргументами является NaN.
Для получения дополнительной информации смотрите NaNs (-check-nan).
Проверка работает почти тем же способом проверкой Invalid operation on floats. Проверка Invalid Use of Standard Library Routine работает над стандартными библиотечными функциями, в то время как проверка Invalid Operation on Floats работает над числовыми операциями, включающими переменные с плавающей точкой.
Ошибка переполнения: ошибка переполнения происходит, если результат функции переполняется. Определение переполнения варьируется на основе того, позволяете ли вы неличные плавания, и на основе округляющихся режимов вы задаете. Если вы позволяете неличные плавания, но указываете, что вас нужно предупредить о бесконечных результатах, ошибка переполнения происходит, если функция возвращает бесконечность, и сами аргументы не являются бесконечностью. Для получения дополнительной информации смотрите Infinities (-check-infinite).
Проверка работает таким же образом проверкой Overflow. Проверка Invalid Use of Standard Library Routine работает над стандартными библиотечными функциями, в то время как проверка Overflow работает над числовыми операциями, включающими переменные с плавающей точкой.
Аргумент недопустимого указателя: Для функций, таких как frexp тот берут аргументы указателя, проверки верификации, если это допустимо, чтобы разыменовать указатель. Например, указатель не является ПУСТЫМ или не указывает внешние позволенные границы.
Проверка ищет эти ошибки в последовательности.
Если проверка находит определенную доменную ошибку, она не ищет ошибку переполнения.
Если проверка находит возможную доменную ошибку, она ищет ошибку переполнения только для путей к выполнению, где доменная ошибка не происходит.
Проверка на каждую ошибку саму может состоять из нескольких условий, которые также проверяются в последовательности. Каждая проверка выполнена только для тех путей к выполнению, куда предыдущая проверка передает.
Проверка Invalid Use of Standard Library Routine покрывает следующие стандартные программы, их версии с одинарной точностью с суффиксным f (если у них есть один), и их долгие двойные версии с суффиксным l. Проверка работает точно таким же образом на C и Код С++.
acos
acosh
asin
asinh
atan
atanh
ceil
cos
cosh
exp
exp2
expm1
fabs
floor
log
log10
log1p
logb
round
sin
sinh
sqrt
tan
tanh
trunc
cbrt
Проверка Invalid Use of Standard Library Routine покрывает следующие стандартные программы, их версии с одинарной точностью с суффиксным f (если у них есть один), и их долгие двойные версии с суффиксным l. Проверка работает точно таким же образом на C и Код С++.
atan2
fdim
fma
fmax
fmin
fmod
frexp
hypot
ilogb
ldexp
modf
nextafter
nexttoward
pow
remainder
Consider non finite floats (-allow-non-finite-floats) | Float rounding mode (-float-rounding-mode)
