Exponenta Banner

Верификация программы автоматического доказательства кода

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

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

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

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

Verify module or library (-main-generator)Сгенерируйте main функционируйте, если исходные файлы являются модулями или библиотеками, которые не содержат main
Show global variable sharing and usage only (-shared-variables-mode)Вычислите совместное использование глобальной переменной и использование, не запуская полный анализ
Verify initialization section of code only (-init-only-mode)Проверяйте один только код инициализации на ошибки времени выполнения и другие проблемы
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

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

Проверьте Приложение C Без основной Функции

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

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

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

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

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

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

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

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