Внешние ограничения на анализ Polyspace сгенерированного кода

Когда вы проверяете сгенерированный код на ошибки или ошибки времени выполнения, можно выбрать, выполнить ли проверку для всех значений входа или определенной области значений значений. Можно извлечь входной диапазон из модели Simulink®.

Аналогично, можно использовать фиксированное значение в настраиваемых параметрах или области значений значений. Можно также проверять, находятся ли выходные значения в пределах определенной области значений.

Извлеките внешние ограничения из модели

Рассмотрите эту простую модель с блоком Inport, блоком Gain и блоком Outport. Предположим, что сигнал в блоках Inport и Outport и параметре усиления блока Gain имеет минимальное и максимальное значение.

Можно анализировать код, сгенерированный из этой модели с этими минимальными и максимальными значениями. На вкладке Apps выберите Polyspace Code Verifier. Затем на вкладке Polyspace выберите Settings. Задайте эти параметры конфигурации:

  • Входной параметр: выберите Use specified minimum and maximum values. Анализ Программы автоматического доказательства Кода проверяет сгенерированный код в заданной области значений от блока Inport. Анализ Средства поиска Ошибки использует эту информацию, чтобы исключить ложные положительные стороны.

    Значение по умолчанию: Эта опция выбрана.

  • Настраиваемые параметры: Выберите Use specified minimum and maximum values.

    Значение по умолчанию: Эта опция не выбрана. Анализ использует фиксированное значение усиления блока Gain (значение 2 в примере).

    Для анализа, чтобы рассмотреть область значений вместо фиксированного значения, параметры должны быть настраиваемыми и не встроенные. Смотрите поведение параметра По умолчанию.

  • Вывод : выберите Verify outputs are within minimum and maximum values. Анализ Программы автоматического доказательства Кода создает красную проверку, если выходные параметры превышают диапазон, указанный на блоке Outport. См. также Correctness condition.

    Значение по умолчанию: Эта опция не выбрана. Анализ Программы автоматического доказательства Кода не проверяет выходные значения.

После анализа, чтобы проверять, используется ли ограниченное значение области значений, смотрите один из этих файлов:

  • Ограничительный XML-файл спецификации modelname_drs.xml в папке results_modelname\modelname.

  • Файл проекта Polyspace® modelname.prpsj в папке results_modelname.

    Откройте этот файл в пользовательском интерфейсе Polyspace. В настройке проекта смотрите извлеченные ограничения, заданные для опции Constraint setup (-data-range-specifications).

Классы памяти, поддержанные для ограничительной экстракции

Чтобы позволить ограничительную экстракцию из модели Simulink, сигналы и параметры должны иметь типы данных в определенных классах памяти. Для получения дополнительной информации на классах памяти, смотрите, Выбирают Storage Class for Controlling Data Representation in Generated Code (Embedded Coder).

Общие классы памяти

Класс памятиПоддерживаемое ограничение сигналаПоддерживаемое ограничение параметра
AutoДа

Да

ExportedGlobalДаДа
ImportedExternДаДа
ImportedExternPointerДаДа
Model defaultДаДа

Другие классы памяти

Класс памятиПоддерживаемое ограничение сигналаПоддерживаемое ограничение параметра
BitFieldДаДа
CompilerFlagНетНет
ConstНетДа
ConstVolatileНетДа
DefineНетНет
ExportToFileДаДа
FileScopeДаНет
GetSetНетНет
ImportedDefineНетНет
ImportFromFileНетНет
StructНетНет
VolatileДаДа

Похожие темы