Class (-class-analyzer)

Задайте классы, которые вы хотите проверить

Описание

Эта опция влияет только на анализ Code Prover.

Задайте классы, которые Polyspace® использует, чтобы сгенерировать main.

Задать опцию

Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Code Prover Verification. Смотрите Зависимости для других опций, которые вы также должны включить.

Командная строка и файл опций: Используйте опцию -class-analyzer. См. «Информация о командной строке».

Зачем использовать эту опцию

Если вы проверяете модуль или библиотеку, Code Prover генерирует main функция, если она не существует. Если a main существует, в анализе используются существующие main.

Используйте эту опцию и опцию Functions to call within the specified classes (-class-analyzer-calls) чтобы задать методы классов, которые сгенерированы main должен вызвать. Если метод класса не вызывается прямо или косвенно из mainпрограммное обеспечение не анализирует метод.

Настройки

По умолчанию: all

all

Polyspace может использовать все классы для генерации main. Сгенерированный main вызывает методы, которые вы задаете, используя Functions to call within the specified classes.

none

Сгенерированный main невозможно вызвать какой-либо метод класса.

custom

Polyspace может использовать классы, которые вы задаете, чтобы сгенерировать main. Сгенерированный main вызывает методы из классов, которые вы задаете используя Functions to call within the specified classes.

Зависимости

Использовать эту опцию можно только в том случае, если все из следующих значений true:

Совет

Если вы выбираете none для этой опции Polyspace не будет проверять методы класса, которые вы явным образом не вызываете в коде.

Информация о командной строке

Параметр: -class-analyzer
Значение: all | none | custom = class1[, class2,...]
По умолчанию: all
Пример (Code Prover): Polyspace Code Prover -sources file_name -main-generator анализатора класса custom = myClass1, myClass2
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -main-generator анализатора класса custom = myClass1, myClass2