После верификации вы видите в Code covered by verification графиках, что значительный фрагмент вашего кода не была проверяем на ошибки времени выполнения.
Например, на следующем графике на панели Dashboard показано, что 75% ваших функций не были проверены на ошибки времени выполнения. (В проверенных функциях не проверялось только 7% операций.)
Процент непроверенного кода в Code covered by verification графика охватывает:
Функции и операции, которые не проверяются, поскольку доказано, что они недоступны.
Они выглядят серыми на панели Source.
Функции и операции, которые не доказаны недостижимыми, но не проверены по какой-либо другой причине.
Они выглядят черными на панели Source.
Щелкните график Code covered by verification, чтобы увидеть список незапрещенных функций.
Если некоторые файлы не удается скомпилироваться, Polyspace® анализ продолжается с оставшимися файлами. Однако анализ не проверяет несопоставленные файлы на ошибки времени выполнения.
Чтобы увидеть, не скомпилировались ли некоторые файлы, проверьте панель Output Summary или Dashboard. Чтобы убедиться, что все файлы скомпилировались перед анализом, используйте опцию Stop analysis if a file does not compile (-stop-if-compile-error).
Исправьте ошибки компиляции и повторите анализ.
Для получения дополнительной информации о:
Как работает компиляция Polyspace, см. Раздел «Устранение неполадок компиляции и связывание ошибок».
Конкретные ошибки компиляции см. в разделе Поиск и устранение ошибок компиляции.
У вас есть красный или серый чек к началу иерархии вызовов функций. Проверки красного или серого цвета могут привести к последующему снятию флажка с кода.
Красный чек: Верификация не проверяет последующие операции в блоке кода, содержащем красный чек.
Серый чек: Серые чеки указывают на недостижимый код. Верификация не проверяет операции в недоступном коде на наличие ошибок времени выполнения.
Если вы вызываете функции из неотключенного блока кода, верификация также не проверяет эти функции. При наличии красной или серой проверки в начале иерархии вызовов функции в иерархии могут не проверяться. Вы получаете значительное количество непроверенного кода.
Например, в следующем коде проверяется только 1 из 4 функций, и график Procedure показывает 25%. Функции func_called_from_unreachable_1, func_called_from_unreachable_2 и func_called_after_red не проверяются. Только main проверяется.
void func_called_from_unreachable_1(void) {
}
void func_called_from_unreachable_2(void) {
}
void func_called_after_red(void) {
}
int glob_var;
void main(void) {
int loc_var;
double res;
glob_var=0;
glob_var++;
if (glob_var!=1) {
func_called_from_unreachable_1();
func_called_from_unreachable_2();
}
res=0;
/* Division by zero occurs in for loop */
for(loc_var=-10;loc_var<10;loc_var++) {
res += 1/loc_var;
}
func_called_after_red();
}
Посмотрите, main ли функция или другая функция Tasks имеет красные или серые проверки. Проверьте, вызывается ли большая часть функций из последующего незапрещенного кода.
Для перехода от main опустите иерархию вызовов функций и идентифицируйте, с чего начинается снятый код, используйте функции навигации на панели Call Hierarchy. Если по умолчанию панель не отображается, выберите Window > Show/Hide View > Call Hierarchy. Для получения дополнительной информации см. раздел «Иерархия вызовов».
Кроме того, можно рассмотреть произвольную отмененную функцию и выяснить, почему она не проверяется. Посмотрите, применяются ли те же аргументы ко многим функциям. Чтобы обнаружить, не вызывается ли функция вообще из точки входа или вызывается из недоступного кода, используйте опцию Detect uncalled functions (-uncalled-function-checks).
Проверьте красный или серый чеки и исправьте их.
Вы не указали необходимые опции анализа. При неправильном указании следующие опции могут вызвать неконтролируемый код:
Опции многозадачности: Если вы проверяете многозадачный код, с помощью этих опций вы задаете свои функции точки входа.
Возможные ошибки в спецификации включают:
Вы ожидали автоматического обнаружения параллелизма, чтобы обнаружить создание потока, но вы используете примитивы создания потока, которые еще не поддерживаются для автоматического обнаружения.
С ручной настройкой многозадачности вы не указали все свои точки входа.
Основные опции генерации: Через эти опции вы генерируете main функция, если она не существует в вашем коде. При проверке модулей или библиотек используются эти опции.
Вы не указали все функции, которые сгенерированы main должен вызвать.
Входы и опции упругости: Через эти опции, вы ограничиваете области значений переменных от вне вашего кода или силы упругости функций.
Возможные ошибки в спецификации включают:
Вы задали области значений переменных, которые являются слишком узкими, что приводит к тому, что в противном случае достижимый код становится недоступным.
Вы непреднамеренно уперлись в некоторые функции.
Макросы: Через эти опции вы задаете или не определяете макросы препроцессора.
Возможно, вам придется явным образом задать макрос, который ваш компилятор рассматривает неявно, как определено.
Проверьте свои опции в предыдущем порядке. Если ваши спецификации неправильны, исправьте их.
main Функция не прекращаетсяЭта причина применяется только к многозадачному коду, когда не проверяются целые функции точки входа.
Если вы конфигурируете опции многозадачности вручную, необходимо следовать ограничениям модели многозадачности Polyspace. В частности, main функция не должна содержать бесконечный цикл или ошибку времени выполнения. В противном случае функции точки входа не проверяются.
Например, в этом примере task2 не проверяется, даже если он задан как точка входа. Причина - бесконечный цикл в main функция.
void performTask1Cycle(void);
void performTask2Cycle(void);
void main() {
while(1) {
performTask1Cycle();
}
}
void task2() {
while(1) {
performTask2Cycle();
}
}Вы видите while ключевое слово в main функция подчеркнута штриховым красным цветом. Подсказка указывает, что цикл может не завершиться.
Аналогично, если происходит ошибка времени выполнения, вызов функции, приводящий к ошибке времени выполнения, подчеркивается штриховым красным цветом с сопутствующей подсказкой.
main ФункцияИсправьте причину, по которой main функция не завершается.
Если причиной является определенная ошибка времени выполнения (красная проверка), исправьте ошибку.
Если причиной является бесконечный цикл, посмотрите, почему цикл должен быть бесконечным.
Если бесконечный цикл в main функция представляет циклическую задачу, завершает main и переместите бесконечный цикл в другую функцию точки входа. Вы можете внести это изменение только в целях анализа Polyspace, не изменяя фактически свои main функция. Смотрите Настройку многозадачного анализа Polyspace вручную.