-stub-embedded-coder-lookup-table-functions
)Тупик автоматически сгенерировал функции, которые используют интерполяционные таблицы и моделируют их более точно
Эта опция доступна только для сгенерированного кода модели. Опция релевантна, только если вы генерируете код из модели Simulink®, которая использует блоки Интерполяционной таблицы с помощью продуктов генерации кода MathWorks®.
Укажите, что верификация должна заблокировать автоматически сгенерированные функции, которые используют определенные виды интерполяционных таблиц в их теле. Интерполяционные таблицы в этих функциях используют линейную интерполяцию и не позволяют экстраполяцию. Таким образом, результат использования интерполяционной таблицы всегда находится между нижними и верхними границами таблицы.
Если при запуске верификацию от Simulink, используйте опцию интерполяционные таблицы Тупика (Polyspace Code Prover) в Параметрах конфигурации Simulink, который выполняет ту же задачу.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта Polyspace® опция находится на узле Inputs & Stubbing.
Командная строка: Используйте опцию -stub-embedded-coder-lookup-table-functions
. Смотрите информацию о командной строке.
Если вы используете эту опцию, верификация более точна и имеет меньше оранжевых проверок. Верификация функций интерполяционной таблицы обычно неточна. Программное обеспечение должно сделать определенные предположения об этих функциях. Чтобы постараться не пропускать ошибку времени выполнения, верификация принимает, что результат использования интерполяционной таблицы в полном спектре, позволенном типом данных результата. Это предположение может вызвать много бездоказательных результатов (оранжевые проверки), когда функция интерполяционной таблицы вызвана. При помощи этой опции вы сужаете предположение. Для функций, которые используют интерполяционные таблицы с линейной интерполяцией и никакой экстраполяцией, результат, по крайней мере, в границах таблицы.
Опция релевантна, только если ваша модель имеет блоки Интерполяционной таблицы. В сгенерированном коде функции, соответствующие блокам Интерполяционной таблицы также, используют интерполяционные таблицы. Имена функций следуют определенным соглашениям. Верификация использует соглашения о присвоении имен идентифицировать, используют ли интерполяционные таблицы в функциях линейную интерполяцию и никакую экстраполяцию. Верификация затем заменяет такие функции на тупики для более точной верификации.
Для автоматически сгенерированных функций, которые используют интерполяционные таблицы с линейной интерполяцией и никакой экстраполяцией, верификацией:
Не проверяет на ошибки времени выполнения в теле функции.
Вызывает функциональный тупик вместо фактической функции на сайтах вызова функции. Тупик гарантирует, что результат использования интерполяционной таблицы в границах таблицы.
Чтобы идентифицировать, использует ли интерполяционная таблица в функции линейную интерполяцию и никакую экстраполяцию, верификация использует имя функции. В ваших результатах анализа вы видите, что функция не анализируется. Если вы устанавливаете свой курсор на имя функции, вы видите следующее сообщение:
Function has been recognized as an Embedded Coder Lookup-Table function. It was stubbed by Polyspace to increase precision. Unset the -stub-embedded-coder-lookup-table-functions option to analyze the code below.
Верификация не блокирует автоматически сгенерированные функции то использование интерполяционные таблицы.
Опция применяется только к автоматически сгенерированным функциям. Если вы интегрируете свою собственную S-функцию C/C++ с помощью интерполяционных таблиц с моделью, эти функции не следуют соглашениям о присвоении имен для автоматически сгенерированных функций. Опция не заставляет их быть заблокированными. Если вы хотите то же поведение для своих рукописных функций интерполяционной таблицы как автоматически сгенерированные функции, используйте опцию -code-behavior-specifications
и сопоставьте свою функцию с __ps_lookup_table_clip
функция.
Если при запуске верификацию от Simulink, опция идет по умолчанию. В целях сертификации, если вы хотите, чтобы ваш инструмент верификации был независим от инструмента генерации кода, выключают опцию.
Параметр: -stub-embedded-coder-lookup-table-functions |
Значение по умолчанию: на |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |