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 Code Prover Server
Поддержка