Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки Invalid use of standard library routine. Для получения описания примеров проверки и кода смотрите Invalid use of standard library routine.
Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.
Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.
Выберите проверку на панели Results List. Дополнительные сведения о проверке см. на панели Result Details. Проверка красная или оранжевая из-за недопустимых аргументов функции.
Причина проверки красного или оранжевого цвета зависит от используемой стандартной функции библиотеки. В следующей таблице показаны возможные причины некоторых из обычно используемых функций.
| Функция | Причина проверки красного или оранжевого цвета | |
|---|---|---|
islower, isdigit, и другие функции обработки символов в ctype.h | Значение аргумента может находиться вне допустимого для Обратите внимание, что можно использовать макрос | |
Функции в | Программа последовательно проверяет наличие нескольких видов ошибок. Программа выполняет каждую проверку только для тех путей выполнения, где прошла предыдущая проверка. Некоторые примеры приведены ниже. Дополнительные сведения и список функций см. в разделе Недопустимое использование стандартных стандартных программ с плавающей точкой библиотеки. | |
sqrt | Значение аргумента может быть отрицательным. | |
pow | Первый аргумент может быть отрицательным, в то время как второй аргумент является нецелым числом. | |
exp, exp2, или гиперболические функции | Аргумент может быть настолько большим, что результат превышает значение, разрешенное для double. | |
log | Аргумент может быть нулем или отрицательным. | |
asin или acos | Аргумент может находиться вне области значений [-1,1]. | |
tan | Аргумент может иметь значение HALF_PI. | |
acosh | Аргумент может быть меньше 1. | |
atanh | Аргумент может быть больше 1 или меньше -1. | |
fprintf, fscanf, и другие функции обработки файлов | Аргумент указателя на файл может быть нечитаемым. Для примера это может быть NULL. | |
| Функции, которые берут строковые аргументы | Строковый аргумент может быть недопустимой строкой. Например, это не заканчивается завершающим '\0'. | |
memmove или memcpy | Третий аргумент этой функции задает количество байтов для копирования из второго в первый аргумент. Это число может превысить память, выделенную первому или второму аргументу. | |
Посмотрите, можно ли проследить оранжевую проверку до допущения Polyspace, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.
Например, вы получаете значение из неопределенной функции и выполняете sqrt операция на нем. Затем:
Polyspace принимает, что функция может вернуть отрицательное значение.
Поэтому программное обеспечение производит оранжевую проверку Invalid Use of Standard Library Routine на sqrt вызов функции.
Если вы знаете, что функция возвращает положительное значение, чтобы избежать оранжевого цвета, можно задать ограничение на возврат значение вашей функции. См. Допущения об упрямых функциях. Также добавьте комментарий и обоснование, описывающие, почему вы не изменили свой код.
Для получения дополнительной информации смотрите Допущения анализа Code Prover.
