Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки Invalid use of standard library routine. Для описания проверки и примеров кода, смотрите Invalid use of standard library routine.
Иногда, особенно для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать опцию анализа, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.
Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Программы автоматического доказательства Кода в Пользовательском интерфейсе Рабочего стола 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. | |
fprintffscanf, и другие функции обработки файла | Аргумент указателя файла может быть нечитаемым. Например, это может быть NULL. | |
| Функции тот берут аргументы строки | Аргумент строки может быть недопустимой строкой. Например, это не заканчивается завершающим работу '\0'. | |
memmove или memcpy | Третий аргумент этой функции задает количество байтов, чтобы скопировать от второго до первого аргумента. Этот номер может превысить память, выделенную первому или второму аргументу. | |
Смотрите, можно ли проследить оранжевую проверку до предположения Polyspace, которое происходит ранее в коде. Если предположение не сохраняется в вашем случае, добавьте комментарий или выравнивание в вашем результате или коде. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Выравнивания.
Например, вы получаете значение из неопределенной функции и выполняете sqrt операция на нем. То:
Polyspace принимает, что функция может возвратить отрицательное значение.
Поэтому программное обеспечение производит оранжевый Invalid Use of Standard Library Routine, проверяют sqrt вызов функции.
Если вы знаете, что функция возвращает положительное значение, чтобы избежать оранжевого, можно задать ограничение на возвращаемое значение функции. Смотрите Предположения О Заблокированных Функциях. Альтернативно, добавьте комментарий и выравнивание, описывающее, почему вы не изменили свой код.
Для получения дополнительной информации смотрите Аналитические Предположения Программы автоматического доказательства Кода.
