Exponenta Banner

Входные параметры и блокирование

Укажите диапазоны для глобальных переменных и функций

Чтобы задать локальные предположения, используйте входные параметры и блокирующие опции. Например, можно ограничить области значений некоторых переменных из внешних источников, тупик некоторые неточно анализируемые функции для более точного анализа или подавить нарушения правила кодирования из некоторых файлов. Предположения помогают сузить особое внимание вашего анализа к результатам анализа, которые более значимы. Для глобальных предположений, которые применяются к определенному построению кода во всех файлах и функциях, используйте опции Предположений Верификации.

Аналитические опции

развернуть все

Constraint setup (-data-range-specifications)Ограничьте глобальные переменные, входные параметры функции и возвращаемые значения заблокированных функций
Ignore default initialization of global variables (-no-def-init-glob)Рассмотрите глобальные переменные как неинициализированные, если явным образом не инициализировано в коде
No STL stubs (-no-stl-stubs)Не используйте реализации Polyspace функций в Стандартной библиотеке шаблонов
Functions to stub (-functions-to-stub)Задайте функции к тупику во время анализа
Generate stubs for Embedded Coder lookup tables (-stub-embedded-coder-lookup-table-functions)Тупик автоматически сгенерировал функции, которые используют интерполяционные таблицы и моделируют их более точно
Generate results for sources and (-generate-results-for)Задайте файлы, на которых вы хотите результаты анализа
Do not generate results for (-do-not-generate-results-for)Задайте файлы, на которых вы не хотите результатов анализа

Темы

Задайте аналитические опции Polyspace

Задайте аналитические опции Polyspace® в пользовательском интерфейсе Polyspace, других IDE-s или скриптах.

Задайте внешние ограничения

Ограничьте переменные диапазоны и спецификации указателя для более точного анализа.

Внешние ограничения для анализа Polyspace

Ищите ограничения, которые можно применить на глобальные переменные, входные параметры функции и заблокированные функции.

Обеспечьте контекст для верификации кода С

Изучите, какой внешний контекст можно обеспечить, чтобы сузить предположения верификации по умолчанию.

Обеспечьте контекст для верификации кода С++

Изучите, какой внешний контекст можно обеспечить, чтобы сузить предположения верификации по умолчанию.

Документация Polyspace Code Prover
Поддержка