Верификация застревает в определенный момент в течение долгого времени. Иногда, после того, как период неактивности превышает внутренний порог, остановки верификации, или вы получаете сообщение об ошибке:
The analysis has been stopped by timeout.
Для крупных проектов с несколькими сотнями исходных файлов или миллионов строк кода, вы можете столкнуться с той же проблемой в другом отношении. Верификация останавливается с сообщением об ошибке:
Fatal error: Not enough memory
Если у вас есть многожильная система больше чем с четырьмя процессорами, попытайтесь увеличить число процессоров при помощи опции -max-processes. По умолчанию верификация использует до четырех процессоров. Если у вас есть меньше чем четыре процессора, верификация использует максимальный доступный номер. У вас должно быть по крайней мере 4 Гбайт RAM на процессор для анализа. Например, если ваша машина имеет 16 Гбайт RAM, не используйте эту опцию, чтобы задать больше чем четыре процессора.
Если верификация все еще занимает слишком много времени, чтобы улучшить скорость и сделать верификацию быстрее, попробуйте одно из решений ниже.
В некоторых случаях проверки антивирусного программного обеспечения могут заметно замедлить анализ Polyspace®. Это сокращение происходит, потому что программное обеспечение проверяет временные файлы, произведенные анализом Polyspace.
Проверяйте выполнение процессов и смотрите, использует ли антивирус большой объем памяти.
Смотрите ошибку или медленные запуски от дисковой дефрагментации и антивирусного программного обеспечения.
Время верификации зависит от размера и сложности вашего кода.
Если приложение содержит больше, чем 100 000 строк кода, верификация может иногда занимать много времени. Даже для малых приложений, верификация может занять много времени, если она включает сложности, такие как структуры со многими уровнями вложения или несколькими уровнями искажения через указатели. Вы видите, что количество линий, исключая комментарии к началу анализа входит в систему ваша папка результатов. Ищите строку:
Number of lines without comments
Однако, если верификация с опциями по умолчанию берет необоснованно долго или останавливается в целом, существует несколько стратегий уменьшать время верификации. Каждая стратегия включает сокращение сложности верификации в некотором роде.
Используйте Polyspace Bug Finder™ сначала, чтобы найти дефекты в вашем коде. Некоторые дефекты, которые находки Polyspace Bug Finder могут перевести в красную ошибку в Polyspace Code Prover™. Если вы фиксируете эти дефекты, используйте Polyspace Code Prover в более строгой верификации.
Можно разделить приложение на несколько модулей. Проверьте каждый модуль независимо от других модулей. Можно рассмотреть полные результаты для одного модуля, в то время как верификация других модулей все еще запускается.
Можно позволить программному обеспечению построить приложение из модулей. Программное обеспечение делит ваши исходные файлы на несколько модулей, таким образом, что взаимозависимость между модулями как можно меньше. Используйте polyspace-modularize команда в polyspaceroot\polyspace\bin-h опция.
Можно выполнить верификацию файла файлом. Каждый файл составляет модуль отдельно. Смотрите Verify files independently (-unit-by-unit).
Когда вы делите свое законченное приложение на модули, каждый модуль имеет некоторых информационных пропавших без вести. Например, один модуль может содержать вызов функции, которая задана в другом модуле. Программное обеспечение делает определенные предположения о неопределенных функциях. Если предположения более широки, чем фактическое представление функции, вы видите увеличение оранжевых проверок от сверхприближения. Например, управление обработкой ошибок функциональная сила возвращает int значение, которое является или 0 или 1. Однако то, когда Polyspace не может найти функциональное определение, он принимает, что функция возвращает все возможные значения, допускало int переменная. Можно сузить предположения путем определения внешних ограничений. Смотрите Constraint setup (-data-range-specifications).
При модульном исполнении приложения вручную, можно следовать собственным подходом модуляризации. Например, можно скопировать только критические файлы, которыми вы обеспокоены в один модуль и проверяете их. Можно представлять остающиеся файлы посредством внешних ограничений, если вы уверены, что ограничения представляют недостающий код искренне. Например, ограничения на неопределенную функцию представляют функцию искренне, если они представляют функциональное возвращаемое значение и также воспроизводят другие соответствующие побочные эффекты функции. Чтобы задать внешние ограничения, используйте опцию Constraint setup (-data-range-specifications).
Если ваша верификация занимает слишком много времени, используйте более низкий уровень точности или более низкий уровень верификации. Зафиксируйте красные ошибки, найденные на том уровне, и повторно выполните верификацию.
Уровень точности определяет алгоритм, используемый в верификации. Более высокая точность приводит к большему количеству доказанных результатов, но также и требует большего количества времени верификации. Для получения дополнительной информации смотрите Precision level (-O).
Уровень верификации решает, что Polyspace числа раз работает на вашем исходном коде. Для получения дополнительной информации смотрите Verification level (-to).
Результаты верификации более низкой точности могут содержать больше оранжевых проверок. Оранжевая проверка указывает, что анализ рассматривает подозреваемого операции, но не может доказать присутствие или отсутствие ошибки времени выполнения. Необходимо рассмотреть оранжевую проверку полностью, чтобы определить, можно ли сохранить операцию. Путем увеличения числа оранжевых проверок вы эффективно увеличиваете время, вы тратите рассмотрение результатов верификации. Поэтому используйте эти стратегии, только если верификация занимает слишком много времени.
И для лучшей удобочитаемости вашего кода и в течение более короткого времени верификации, можно уменьшать сложность кода. Polyspace вычисляет метрики сложности кода из вашего приложения и позволяет вам ограничивать те метрики ниже предопределенных значений.
Для получения дополнительной информации см.:
Метрики кода (Polyspace Code Prover Access): Список метрик сложности кода и их рекомендуемых верхних пределов
Вычислите Метрики сложности кода: Как установить пределы для метрик сложности кода
В зависимости от вашей ситуации можно выбрать масштабирующиеся опции, чтобы включить определенные приближения. Часто, предупреждающие сообщения указывают, что необходимо использовать те опции, чтобы уменьшать верификацию.
| Ситуация | Опция |
|---|---|
| Ваш код содержит структуры, которые являются многими уровнями глубоко. | Depth of verification inside structures (-k-limiting) |
| Журнал верификации содержит предложения, чтобы встроить определенные функции. | Inline (-inline) |
Можно попытаться удалить код из сторонних библиотек. Программное обеспечение использует тупики в функциях, которые не заданы в файлах, заданных для анализа Polyspace.
Несмотря на то, что аналитическое время уменьшается, вы видите увеличение оранжевых проверок из-за предположений Polyspace о заблокированных функциях. Можно ограничить заблокированные функции с помощью опции Constraint setup (-data-range-specifications).
Если ваш код предназначается для многозадачности, и вы обеспечиваете много Задач, верификация может занять много времени. Соблюдающее предупреждение может появиться:
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).
Для примера использования функции обертки как точка входа смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.