Верификация застряла в определенной точке надолго. Иногда, после того, как период бездействия превышает внутренний порог, верификация останавливается или вы получаете сообщение об ошибке:
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 Bug Finder™ сначала, чтобы найти дефекты в вашем коде. Некоторые дефекты, которые обнаруживает Polyspace Bug Finder, могут привести к красной ошибке в Polyspace Code Prover™. После устранения этих дефектов используйте Polyspace Code Prover для более строгой верификации.
Можно разделить приложение на несколько модулей. Проверьте каждый модуль независимо от других модулей. Можно просмотреть полные результаты для одного модуля, в то время как верификация других модулей все еще выполняется.
Вы можете позволить программному обеспечению модуляризировать ваше приложение. Программное обеспечение разделяет ваши исходные файлы на несколько модулей таким образом, чтобы взаимозависимость между модулями была как можно меньше.
Запустите быструю начальную верификацию с самой низкой точностью и уровнем верификации. См. Precision level (-O) и Verification level (-to).
Выберите Tools > Run Modularize.
Программа отображает график между количеством модулей и количеством переменных/функций кросс-модуля или сложностью каждого модуля. Используя этот график для руководства, выберите количество модулей, в которые должен быть разбит проект. Вы должны пойти на компромисс между зависимостью кросс-модулей и сложностью каждого модуля.
Выберите вертикальную серую область на графике, соответствующем количеству выбранных модулей. Программное обеспечение разделяет ваш проект на столько модулей.
Модуляризировать приложение можно из командной строки. Используйте polyspace-modularize команда в polyspaceroot\ polyspace\bin-h опция.
При запуске верификации в пользовательском интерфейсе можно создать несколько модулей в проекте и скопировать исходные файлы в эти модули. Чтобы начать, щелкните правой кнопкой мыши проект и выберите Create new module.
Можно выполнить верификацию файла по файлам. Каждый файл сам по себе образует модуль. См. Verify files independently (-unit-by-unit).
Когда вы делите полное приложение на модули, у каждого модуля отсутствует некоторая информация. Например, один модуль может содержать вызов функции, заданный в другом модуле. Программа делает определенные допущения относительно неопределенных функций. Если предположения шире, чем фактическое представление функции, вы видите увеличение оранжевых проверок от сверхприближения. Например, функция управления ошибками может вернуть int значение 0 или 1. Однако, когда Polyspace не может найти определение функции, он принимает, что функция возвращает все возможные значения, разрешенные для int переменная. Можно сузить допущения путем определения внешних ограничений.
При модуляризации приложения вручную можно придерживаться собственного подхода модуляризации. Например, можно скопировать в один модуль только критические файлы, которые вас беспокоят, и проверить их. Вы можете представлять оставшиеся файлы через внешние ограничения, при условии, что вы уверены, что ограничения представляют отсутствующий код достоверно. Например, ограничения на неопределенную функцию представляют функцию достоверно, если они представляют значение возвращаемой функции, а также воспроизводят другие релевантные побочные эффекты функции. Чтобы задать внешние ограничения, используйте опцию Constraint setup (-data-range-specifications).
Если проверка занимает слишком много времени, используйте более низкий уровень точности или более низкий уровень верификации. Исправьте красные ошибки, обнаруженные на этом уровне, и повторите верификацию.
Уровень точности определяет алгоритм, используемый для верификации. Более высокая точность приводит к большему количеству проверенных результатов, но также требует большего времени верификации. Для получения дополнительной информации смотрите Precision level (-O).
Уровень верификации определяет количество раз, когда Polyspace запускается на вашем исходном коде. Для получения дополнительной информации смотрите Verification level (-to).
Результаты верификации более низкой точности могут содержать больше оранжевых проверок. Оранжевая проверка указывает, что анализ рассматривает операцию как подозрительную, но не может доказать наличие или отсутствие ошибки времени выполнения. Необходимо тщательно проверить оранжевый чек, чтобы определить, можно ли сохранить операцию. Увеличивая количество оранжевых проверок, вы эффективно увеличиваете время, затрачиваемое на просмотр результатов верификации. Поэтому используйте эти стратегии только в том случае, если верификация занимает слишком много времени.
Как для лучшей читаемости вашего кода, так и для более короткого времени верификации, можно уменьшить сложность своего кода. Polyspace вычисляет метрики сложности кода из вашего приложения и позволяет вам ограничить эти метрики ниже предопределенных значений.
Для получения дополнительной информации смотрите:
Метрики кода: Список метрик сложности кода и их рекомендуемых верхних пределов
Метрики сложности вычислительного кода: как задать пределы на метрики сложности кода
Запустите менее обширный анализ Code Prover на вашем приложении, который вычисляет только совместное использование и использование глобальных переменных. Затем можно запустить полный компонент анализа по компонентам для обнаружения ошибок времени выполнения. См. 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 чтобы сохранить точный анализ, можно уменьшить количество заданных точек входа. Если вы знаете, что некоторые из функций точки входа не выполняются одновременно, вы не должны указывать их как отдельные точки входа. Можно вызвать эти функции последовательно в функции wrapper, а затем задать функцию wrapper в качестве точки входа.
Например, если известно, что точка входа функционирует 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).
Пример использования функции обертки в качестве точки входа см. в разделе Настройка многозадачного анализа Polyspace вручную.