С продуктом Polyspace® Code Prover™ можно применить верификацию Polyspace к сгенерированному коду Embedded Coder®. Программное обеспечение обнаруживает ошибки времени выполнения в сгенерированном коде и помогает вам определить местоположение и зафиксировать образцовые отказы.
Polyspace может подсветить переполнение для определенных операций, которые законны из-за способа, которым генератор кода реализует эти операции. Рассмотрите следующую модель и соответствующий сгенерированный код.
32 /* Sum: '<Root>/Sum' incorporates: 33 * Inport: '<Root>/In1' 34 * Inport: '<Root>/In2' 35 */ 36 qY_0 = sat_add_U.In1 + sat_add_U.In2; 37 if ((sat_add_U.In1 < 0) && ((sat_add_U.In2 < 0) && (qY_0 >= 0))) { 38 qY_0 = MIN_int32_T; 39 } else { 40 if ((sat_add_U.In1 > 0) && ((sat_add_U.In2 > 0) && (qY_0 <= 0))) { 41 qY_0 = MAX_int32_T; 42 } 43 }
Генератор кода распознает, что самый большой встроенный тип данных является 32-битным. Не возможно насыщать результаты сложений и вычитаний с помощью MIN_INT32 и MAX_INT32 и большего целочисленного типа данных однословного. Вместо этого программное обеспечение обнаруживает переполнение результатов и направление переполнения, и насыщает результат.
Если вы не обеспечиваете выравнивание для оператора сложения на строке 36, верификация Polyspace генерирует оранжевый чек, который указывает на потенциальное переполнение. Верификация не учитывает функцию насыщения строк 37 - 43. Кроме того, функциональность трассировки назад Polyspace Code Prover не идентифицирует причину оранжевой проверки.
Чтобы выровнять по ширине переполнение от операторов, которые законны на Configuration Parameters> Code Generation> панель Comments:
Под Overall control установите флажок Include comments.
Под Auto generate comments установите флажок Operator annotations.
Генератор кода аннотирует сгенерированный код комментариями для Polyspace. Например:
32 /* Sum: '<Root>/Sum' incorporates:
33 * Inport: '<Root>/In1'
34 * Inport: '<Root>/In2'
35 */
36 qY_0 = sat_add_U.In1 +/*MW:OvOk*/ sat_add_U.In2;
Когда вы запускаете верификацию с помощью Polyspace Code Prover, программное обеспечение Polyspace использует аннотации, чтобы выровнять по ширине связанные с оператором оранжевые проверки и присваивает классификацию Not a defect проверкам.