Exponenta Banner

Входы и упругость

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

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

Опции анализа

расширить все

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)Заглушка автогенерированных функций, которые используют интерполяционные таблицы и моделируют их более точно
Libraries used (-library)Задайте библиотеки, которые вы используете в своей программе
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

Поддержка