Проверка застряла в определенной точке надолго. Иногда после того, как период бездействия превышает внутренний порог, проверка прекращается или появляется сообщение об ошибке:
The analysis has been stopped by timeout.
Для крупных проектов с несколькими сотнями исходных файлов или миллионами строк кода эта проблема может возникнуть другим способом. Проверка прекращается с сообщением об ошибке:
Fatal error: Not enough memory
Если у вас многоядерная система с более чем четырьмя процессорами, попробуйте увеличить число процессоров с помощью опции -max-processes. По умолчанию для проверки используется до четырех процессоров. При наличии менее четырех процессоров при проверке используется максимально возможное количество процессоров. Для анализа необходимо иметь не менее 4 ГБ оперативной памяти на процессор. Например, если на компьютере имеется 16 ГБ оперативной памяти, не используйте этот параметр для указания более четырех процессоров.
Если проверка по-прежнему занимает слишком много времени, чтобы повысить скорость и ускорить проверку, попробуйте одно из приведенных ниже решений.
Во время анализа Polyspace ® создает несколько временных файлов. Если папка, используемая для хранения этих файлов, находится на сетевом диске, анализ может замедлиться.
Измените временную папку на путь на локальном диске.
Сведения о том, как Polyspace определяет расположение временной папки, см. в разделе Хранение временных файлов.
В некоторых случаях проверки антивирусного ПО могут заметно замедлить анализ Polyspace. Это уменьшение происходит потому, что программа проверяет временные файлы, созданные в результате анализа Polyspace.
Проверьте запущенные процессы и убедитесь, что антивирус потребляет большой объем памяти.
См. раздел Ошибки или медленные запуски с дисковой дефрагментации и антивирусного ПО.
Время проверки зависит от размера и сложности кода.
Если приложение содержит более 100 000 строк кода, проверка иногда может занять много времени. Даже для небольших приложений проверка может занять много времени, если она сопряжена со сложностями, такими как структуры со многими уровнями вложенности или несколькими уровнями наложения через указатели. В папке результатов можно просмотреть количество строк, исключая комментарии к началу журнала анализа. Поиск строки:
Number of lines without comments
Однако, если проверка с опциями по умолчанию занимает неоправданно много времени или вообще останавливается, существует несколько стратегий сокращения времени проверки. Каждая стратегия предусматривает некоторое снижение сложности проверки.
Сначала используйте функцию «Ошибка Polyspace» Finder™ чтобы найти дефекты в коде. Некоторые дефекты, обнаруженные Polyspace Bug Finder, могут привести к красной ошибке в Polyspace Code Prover™. После устранения этих дефектов используйте средство проверки кода Polyspace для более строгой проверки.
Приложение можно разделить на несколько модулей. Проверьте каждый модуль независимо от других модулей. Можно просмотреть полные результаты для одного модуля, в то время как проверка других модулей все еще выполняется.
Можно разрешить программному обеспечению модулировать приложение. Программное обеспечение делит исходные файлы на несколько модулей, так что взаимозависимость между модулями минимальна.
Выполните быструю начальную проверку с наименьшей точностью и уровнем проверки. Посмотрите Precision level (-O) и Verification level (-to).
Выберите «Сервис» > «Выполнить модуляцию».
Программа отображает график между количеством модулей и количеством межмодульных переменных/функций или сложностью каждого модуля. С помощью этого графика выберите количество модулей, на которые должен быть разделен проект. Необходимо достичь компромисса между кросс-модульной зависимостью и сложностью каждого модуля.
Выберите вертикальную серую область на графике, соответствующую выбранному количеству модулей. Программа разбивает ваш проект на множество модулей.
Приложение можно модулировать из командной строки. Используйте polyspace-modularize команда в polyspaceroot\polyspace\bin-h вариант.
При выполнении проверки в интерфейсе пользователя можно создать несколько модулей в проекте и скопировать исходные файлы в эти модули. Для начала щелкните проект правой кнопкой мыши и выберите «Создать новый модуль».
Можно выполнить пофайловую проверку. Каждый файл сам по себе представляет собой модуль. Посмотрите Verify files independently (-unit-by-unit).
При разделении всего приложения на модули в каждом модуле отсутствует некоторая информация. Например, один модуль может содержать вызов функции, определенной в другом модуле. Программное обеспечение делает определенные предположения относительно неопределенных функций. Если допущения шире, чем фактическое представление функции, появляется увеличение оранжевых чеков от чрезмерного приближения. Например, функция управления ошибками может возвращать int значение, равное 0 или 1. Однако, когда Polyspace не может найти определение функции, предполагается, что функция возвращает все возможные значения, допустимые для int переменная. Можно сузить допущения, указав внешние ограничения.
При модуляции приложения вручную можно использовать собственный подход к модуляризации. Например, можно скопировать в один модуль только критические файлы, о которых идет речь, и проверить их. Остальные файлы можно представить с помощью внешних ограничений при условии, что ограничения точно представляют отсутствующий код. Например, ограничения неопределенной функции точно представляют функцию, если они представляют возвращаемое значение функции, а также воспроизводят другие релевантные побочные эффекты функции. Для задания внешних ограничений используйте опцию Constraint setup (-data-range-specifications).
Если проверка занимает слишком много времени, используйте более низкий уровень точности или более низкий уровень проверки. Исправьте красные ошибки, обнаруженные на этом уровне, и повторите проверку.
Уровень точности определяет алгоритм, используемый для проверки. Более высокая точность приводит к большему количеству подтвержденных результатов, но также требует большего времени проверки. Дополнительные сведения см. в разделе Precision level (-O).
Уровень проверки определяет количество запусков Polyspace в исходном коде. Дополнительные сведения см. в разделе Verification level (-to).
Результаты проверки более низкой точности могут содержать более оранжевые проверки. Оранжевая проверка показывает, что анализ считает операцию подозрительной, но не может доказать наличие или отсутствие ошибки во время выполнения. Необходимо тщательно проверить оранжевый чек, чтобы определить, можно ли сохранить операцию. Увеличивая количество оранжевых чеков, вы эффективно увеличиваете время, затрачиваемое на просмотр результатов проверки. Поэтому используйте эти стратегии только в том случае, если проверка занимает слишком много времени.
Как для лучшей читаемости кода, так и для более короткого времени проверки можно уменьшить сложность кода. Polyspace вычисляет метрики сложности кода из приложения и позволяет ограничить эти метрики ниже предопределенных значений.
Дополнительные сведения см. в разделе:
Метрики кода: Список метрик сложности кода и их рекомендуемые верхние пределы
Метрики сложности вычисляемого кода: как установить ограничения на метрики сложности кода
Выполните менее обширный анализ программы проверки кода в приложении, который вычисляет только общий доступ к глобальным переменным и их использование. Затем можно выполнить полный анализ по компонентам для обнаружения ошибок во время выполнения. Посмотрите Show global variable sharing and usage only (-shared-variables-mode).
В зависимости от ситуации можно выбрать параметры масштабирования, чтобы включить определенные аппроксимации. Часто предупреждающие сообщения указывают на то, что эти параметры необходимо использовать для уменьшения количества проверок.
| Ситуация | Выбор |
|---|---|
| Код содержит структуры с глубиной в несколько уровней. | Depth of verification inside structures (-k-limiting) |
| Журнал проверки содержит предложения по встраиванию определенных функций. | Inline (-inline) |
Можно попытаться удалить код из сторонних библиотек. Программа использует заглушки для функций, которые не определены в файлах, указанных для анализа Polyspace.
Хотя время анализа сокращается, можно увидеть увеличение оранжевых проверок из-за предположений Polyspace о упорных функциях. См. раздел Допущения о упорных функциях.
Если ваш код предназначен для многозадачности и вы предоставляете множество задач, проверка может занять много времени. Может появиться следующее предупреждение:
Warning: Important use of shared variables have been detected,
| verification carry on but to avoid scaling issues
| it roughly approximates shared variables values.
| You may consider adding -force-refined-shared-variables-analysis
option to improve results
Вместо использования опции -force-refined-shared-variables-analysis для сохранения точного анализа можно уменьшить количество указанных точек входа. Если известно, что некоторые функции точки входа не выполняются одновременно, их не нужно указывать как отдельные точки входа. Эти функции можно вызывать последовательно в функции-обертке, а затем указывать функцию-обертку в качестве точки входа.
Например, если известно, что функции точки входа task1, task2, и task3 не выполняйте одновременно:
Определение функции оболочки task который вызывает task1, task2, и task3 во всех возможных последовательностях.
void task() {
volatile int random = 0;
if (random) {
task1();
task2();
task3();
} else if (random) {
task1();
task3();
task2();
} else if (random) {
task2();
task1();
task3();
} else if (random) {
task2();
task3();
task1();
} else if (random) {
task3();
task1();
task2();
} else {
task3();
task2();
task1();
}
}
Вместо task1, task2, и task3, указать task для опции Tasks (-entry-points).
Пример использования функции оболочки в качестве точки входа см. в разделе Настройка многозадачного анализа в многозадачном пространстве вручную.