Exponenta Banner

Верификация Code Prover

Проверьте все приложение или модуль

Чтобы указать, проверяете ли вы полное приложение с main функция или модуль без main function, используйте Код Prover верификации опций. Если вы проверяете модуль, программное обеспечение генерирует main функция для вас. Чтобы настроить сгенерированные main function, используйте эти опции.

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

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

Verify whole applicationОстановите верификацию, если файлы источников являются неполными и не содержат main функция
Show global variable sharing and usage only (-shared-variables-mode)Вычисление совместного использования и использования глобальных переменных без выполнения полного анализа
Verify initialization section of code only (-init-only-mode)Проверьте код инициализации только на ошибки времени выполнения и другие проблемы
Verify module or library (-main-generator)Сгенерируйте main функция, если исходные файлы являются модулями или библиотеками, которые не содержат main
Variables to initialize (-main-generator-writes-variables)Задайте глобальные переменные, которые вы хотите сгенерировать main инициализировать
Initialization functions (-functions-called-before-main)Задайте функции, которые вы хотите сгенерировать main вызов перед другими функциями
Functions to call (-main-generator-calls)Задайте функции, которые вы хотите сгенерировать main вызов после инициализации функций
Verify files independently (-unit-by-unit)Проверьте каждый исходный файл независимо от других исходных файлов
Common source files (-unit-by-unit-common-source)Укажите файлы, которые вы хотите включить в каждый исходный файл во время верификации файла
Main entry point (-main)Укажите расширения Microsoft Visual C++ для main
Analyze class contents only (-class-only)Не анализируйте код, кроме методов класса
Skip member initialization check (-no-constructors-init-check)Не проверяйте, инициализирует ли конструктор классов членов класса
Functions to call within the specified classes (-class-analyzer-calls)Укажите методы класса, которые вы хотите проверить
Class (-class-analyzer)Задайте классы, которые вы хотите проверить
Verify model generated code (-main-generator)Задайте, что main функция должна быть сгенерирована, если она отсутствует в исходных файлах
Parameters (-variables-written-before-loop)Задайте переменные, которые генерирует main необходимо инициализировать перед циклическим циклом кода
Inputs (-variables-written-in-loop)Задайте переменные, которые генерирует main необходимо инициализировать в циклическом цикле кода
Initialization functions (-functions-called-before-loop)Задайте функции, которые сгенерированы main необходимо вызвать перед циклическим циклом кода
Step functions (-functions-called-in-loop)Задайте функции, которые сгенерированы main должен вызвать циклический цикл кода
Termination functions (-functions-called-after-loop)Задайте функции, которые сгенерированы main должен вызываться после циклического цикла кода

Темы

Задайте опции анализа Polyspace

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

Проверьте приложение C без основной функции

Узнайте преимущества написания main вручную функция от автоматической генерации main функция.

Проверьте классы C++

Узнать, как выполнить робастность верификации классов, чтобы это было безопасно для повторного использования.

Предоставление контекста для верификации кода С

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

Предоставление контекста для верификации кода С++

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

Документация Polyspace Code Prover

Поддержка