Exponenta Banner

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

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

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

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

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

Verify whole applicationОстановите верификацию, если исходные файлы являются неполными и не содержат основную функцию
Show global variable sharing and usage only (-shared-variables-mode)Вычислите совместное использование глобальной переменной и использование, не запуская полный анализ
Verify module or library (-main-generator)Сгенерируйте основную функцию, если исходные файлы являются модулями или библиотеками, которые не содержат основное
Variables to initialize (-main-generator-writes-variables)Задайте глобальные переменные, которые вы хотите, чтобы сгенерированное основное инициализировало
Initialization functions (-functions-called-before-main)Задайте функции, которые вы хотите, чтобы сгенерированное основное вызвало перед другими функциями
Functions to call (-main-generator-calls)Задайте функции, которые вы хотите, чтобы сгенерированное основное вызвало после функций инициализации
Verify files independently (-unit-by-unit)Проверьте каждый исходный файл независимо от других исходных файлов
Common source files (-unit-by-unit-common-source)Задайте файлы, которые вы хотите включать с каждым исходным файлом во время файла верификацией файла
Main entry point (-main)Задайте Microsoft Visual C++ расширения основного
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)Укажите, что основная функция должна быть сгенерирована, если она не присутствует в исходных файлах
Parameters (-variables-written-before-loop)Задайте переменные, которые сгенерированное основное должно инициализировать перед циклическим циклом кода
Inputs (-variables-written-in-loop)Задайте переменные, которые сгенерированное основное должно инициализировать в циклическом цикле кода
Initialization functions (-functions-called-before-loop)Задайте функции, которые сгенерированное основное должно вызвать перед циклическим циклом кода
Step functions (-functions-called-in-loop)Задайте функции, которые сгенерированное основное должно вызвать в циклическом цикле кода
Termination functions (-functions-called-after-loop)Задайте функции, которые сгенерированное основное должно вызвать после циклического цикла кода

Темы

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

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

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

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

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

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

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

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

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

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

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