-code-behavior-specifications

Сопоставьте неточно проанализированную функцию со стандартной функцией для точного анализа

Синтаксис

-code-behavior-specifications file

Описание

-code-behavior-specifications file позволяет связывать определенное поведение с элементами кода и изменять результаты проверок этих элементов. Здесь, file XML- файл, которое присваивает определенное поведение элементам кода, таким как функции.

Для образца можно:

  • Сопоставьте ваши функции библиотеки с соответствующими стандартными функциями, которые Polyspace® распознает. Сопоставление со стандартными функциями библиотеки может помочь с улучшением точности или автоматическим обнаружением новых потоков.

  • Укажите, что функция имеет специальное поведение или должна быть подвергнута специальным проверкам.

    Например, можно задать, что функция должна принимать в качестве аргументов только адреса инициализированных переменных или что функция не должна использоваться вообще.

Если вы запускаете верификацию из командной строки, задайте абсолютный путь к XML- файлы или пути относительно папки, из которой вы запускаете команду. Если вы запускаете верификацию из пользовательского интерфейса (только для продуктов рабочего стола), задайте опцию вместе с абсолютным путем к XML- файлом в поле Other. См. Other. Обратите внимание, что отчет, сгенерированный из результатов анализа, показывает только использование этой опции, а не детали того, какое поведение было связано с элементами кода.

Образец файла шаблона code-behavior-specifications-template.xml показывает синтаксис XML. Файл находится в polyspaceroot\ polyspace\verifier\cxx\ где polyspaceroot - папка установки Polyspace.

Если вы используете Polyspace в качестве расширений You Code в IDE, введите эту опцию в файл опций анализа. См. файл опций.

Использование опции для повышения точности

Синтаксис XML-файла: < имя функции = "custom_function«std =» std_function"> </function >

Используйте эту запись в файл XML, чтобы уменьшить количество оранжевых проверок от неточного анализа Кода Prover вашей функции (или ложных срабатываний от неточного анализа Bug Finder). Иногда верификация не анализирует определенные виды функций именно из-за присущих ей ограничений в статической верификации. В этих случаях, если вы находите стандартную функцию, которая является близким аналогом вашей функции, используйте это отображение. Хотя ваша функция сама по себе не анализируется, анализ более точен в тех местах, где вы вызываете функцию. Например, если верификация не может проанализировать вашу функцию cos32 точно и рассматривает полную область значений для его возвращаемого значения, сопоставить его с cos функция для значения возврата в [-1,1].

Эта верификация игнорирует тело вашей функции. Однако верификация эмулирует поведение вашей функции следующими способами:

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

    Например, если вы сопоставили свою функцию cos32 к стандартной функции cos, верификация принимает, что cos32 возвращает значения в [-1,1].

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

    Например, если вы сопоставили свою функцию acos32 к стандартной функции acos, а Invalid use of standard library routine проверка определяет, является ли аргумент acos32 находится в [-1,1].

Функции, которые можно сопоставить, включают:

  • Стандартные функции библиотеки от math.h.

  • Функции управления памятью от string.h.

  • __ps_meminit: Функция, специфичная для Polyspace, которая инициализирует область памяти.

    Иногда верификация не распознает функцию инициализации памяти и производит оранжевый Non-initialized local variable проверьте переменную, которая была инициализирована с помощью этой функции. Если вы знаете, что ваша функция инициализации памяти инициализирует переменную через ее адрес, сопоставьте вашу функцию с __ps_meminit. Чек становится зеленым.

  • __ps_lookup_table_clip: Функция, специфичная для Polyspace, которая возвращает значение в области значений входного массива.

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

    В коде, сгенерированном из моделей, верификация по умолчанию делает это предположение для функций интерполяционной таблицы. Чтобы идентифицировать, использует ли интерполяция в интерполяционной таблице, и нет экстраполяции, верификация использует имена функции. Используйте отображение только для рукописных функций, например, функций в блоке C/C + + S-Function (Simulink). Имена этих функций не соответствуют конкретным соглашениям. Они должны быть явно заданы.

См. также раздел Расширение функций Bug Finder Checkers для стандартных библиотечных функций для пользовательских библиотек.

Использование опции для обнаружения параллелизма

Синтаксис XML-файла: < имя функции = "custom_function«std =» std_function"> </function >

Используйте эту запись в XML- файл для автоматического обнаружения функций и функций создания потоков, которые начинают и заканчивают критические разделы. Polyspace поддерживает автоматическое обнаружение только для определенных семейств многозадачных примитивов. Расширьте поддержку с помощью этой записи XML.

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

См. раздел Расширение проверки дефектов параллелизма для неподдерживаемых многопоточных окружений.

Использование опции для черного списка функций

Этот раздел применяется только к анализу Bug Finder.

Синтаксис XML-кода:

<function name="function_name">
   <behavior name="FORBIDDEN_FUNC">
</function>

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

Смотрите Устаревшие или небезопасные Функции с использованием Bug Finder Checkers.

Использование опции для расширения проверок инициализации

Синтаксис XML-кода:

<function name="function_name">
   <check name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="n"/>
</function>
Номер n определяет, какой аргумент необходимо проверить для инициализации буфера.

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

См.

Использование опции для изменения глобального поведения

Синтаксис XML-кода:

  <global_scope>
    <parameter name="MAX_NUMBER_NESTED_LEVEL_CONTROL_FLOW" value="n1"/>
    <parameter name="MAX_NUMBER_NESTED_LEVEL_INCLUDES" value="n2"/>
    <parameter name="MAX_NUMBER_CONSTANT_IN_ENUMERATION" value="n3"/>
    <parameter name="MAX_NUMBER_MACROS_TRANSLATION_UNIT" value="n4"/>
    <parameter name="MAX_NUMBER_MEMBERS_IN_STRUCT" value="n5"/>
    <parameter name="MAX_NUMBER_NESTED_MEMBERS_IN_STRUCT" value="n6"/>
    <parameter name="NUMBER_SIGNIFICANT_CHARACTER_EXTERNAL_IDENTIFIER" value="n7"/>
    <parameter name="NUMBER_SIGNIFICANT_CHARACTER_INTERNAL_IDENTIFIER" value="n8"/>
  </global_scope>
Здесь, n1,..,n8 задает числовые значения.

Используйте записи n1,..,n6 для следующих параметров, чтобы задать пределы на определенные аспекты вашей программы. Изменения влияют на проверку MISRA C:2012 Rule 1.1.

    • MAX_NUMBER_NESTED_LEVEL_CONTROL_FLOW: Максимально допустимую глубину вложения в операторах потока управления.

    • MAX_NUMBER_NESTED_LEVEL_INCLUDES: Максимальные уровни включения, разрешенные с помощью файлов include.

    • MAX_NUMBER_CONSTANT_IN_ENUMERATION: Максимальное количество констант, разрешенных в перечислении.

    • MAX_NUMBER_MACROS_TRANSLATION_UNITМаксимально допустимое количество макросов в модуле преобразования.

    • MAX_NUMBER_MEMBERS_IN_STRUCT: Максимальное количество представителей в структуре.

    • MAX_NUMBER_NESTED_MEMBERS_IN_STRUCT: Максимально допустимые уровни вложенности в структуре.

Используйте записи n7 и n8 чтобы указать, сколько символов необходимо сравнить, чтобы определить, совпадают ли два идентификатора. Изменения влияют на проверку Правил 5.x.

  • NUMBER_SIGNIFICANT_CHARACTER_EXTERNAL_IDENTIFIER: Количество символов для сравнения с внешними идентификаторами. Внешние идентификаторы являются таковыми, объявленными с глобальными возможностями или классом памяти extern.

  • NUMBER_SIGNIFICANT_CHARACTER_INTERNAL_IDENTIFIER: Количество символов для сравнения с внутренними идентификаторами.

Примеры

Примеры в следующих разделах относятся к анализу Code Prover. Для примеров Bug Finder смотрите:

Задайте отображение стандартной функции

Вы можете адаптировать XML- файл отображения выборки, предоставленный вашей установкой Polyspace, и сопоставить вашу функцию со стандартной функцией.

Предположим, что верификация по умолчанию создает оранжевый User assertion проверьте этот код:

double x = acos32(1.0) ;  
assert(x <= 2.0);
Предположим, вы знаете, что функция acos32 ведет себя как функция acos и возврат значение 0. Вы ожидаете чек на assert оператор должен быть зеленым. Однако верификация считает, что acos32 возвращает любое значение в области значений типов double потому что acos32 точно не анализируется. Чек оранжевый. Чтобы сопоставить вашу функцию acos32 на acos:

  1. Скопируйте файл code-behavior-specifications-template.xml от polyspaceroot\ polyspace\verifier\cxx\ в другое место, например, "C:\Polyspace_projects\Common\Config_files". Измените разрешения на запись в файл.

  2. Чтобы сопоставить функцию со стандартной функцией, измените содержимое XML- файл. Чтобы сопоставить вашу функцию acos32 к стандартной функции библиотеки acos, измените следующий код:

    <function name="my_lib_cos" std="acos"> </function>
    Кому:
    <function name="acos32" std="acos"> </function>

  3. Укажите местоположение файла для верификации:

    • Code Prover:

      polyspace-code-prover -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"
    • Код Code Prover:

      polyspace-code-prover-server -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"

Задайте отображение со стандартной функцией с переделыванием аргумента

Иногда аргументы вашей функции не сопоставляются один в один с аргументами стандартной функции. В этих случаях переделайте аргумент функции в стандартный аргумент функции. Для образца:

  • __ps_lookup_table_clip:

    Эта функция, характерная для Polyspace, принимает только интерполяционный массив таблицы как аргумент и возвращает значения в области значений интерполяционной таблицы. Ваша функция интерполяционной таблицы может иметь дополнительные аргументы помимо самого массива интерполяционной таблицы. В этом случае используйте изменение аргумента, чтобы указать, какой аргумент вашей функции является массивом интерполяционной таблицы.

    Например, предположим, что функция my_lookup_table имеет следующую декларацию:

    double my_lookup_table(double u0, const real_T *table,
                                         const double *bp0);
    Второй аргумент вашей функции my_lookup_table - массив интерполяционной таблицы. В файл code-behavior-specifications-template.xml, добавить этот код:
    <function name="my_lookup_table" std="__ps_lookup_table_clip">
        <mapping std_arg="1" arg="2"></mapping>
    </function>

    Когда вы вызываете функцию:

    res = my_lookup_table(u, table10, bp);
    Эта верификация интерпретирует вызов как:
    res =__ps_lookup_table_clip(table10);
    Верификация принимает, что значение res лежит в области значений значений в table10.

  • __ps_meminit:

    Эта функция, специфичная для Polyspace, принимает адрес памяти в качестве первого аргумента и количество байтов в качестве второго аргумента. Функция принимает, что байты в памяти, начиная с адреса памяти, инициализируются с допустимым значением. Функция инициализации памяти может иметь дополнительные аргументы. В этом случае используйте изменение аргумента, чтобы указать, какой аргумент вашей функции является начальным адресом, а какой - количеством байтов.

    Например, предположим, что функция my_meminit имеет следующую декларацию:

         void my_meminit(enum InitKind k, void* dest, int is_aligned, unsigned int size);
    Вторым аргументом вашей функции является начальный адрес, а четвертым аргументом - количество байтов. В файл code-behavior-specifications-template.xml, добавить этот код:
    <function name="my_meminit" std="__ps_meminit">
        <mapping std_arg="1" arg="2"></mapping>
        <mapping std_arg="2" arg="4"></mapping>
    </function>

    Когда вы вызываете функцию:

    my_meminit(INIT_START_BY_END, &buffer, 0, sizeof(buffer));
    Эта верификация интерпретирует вызов как:
    __ps_meminit(&buffer, sizeof(buffer));
    Эта верификация принимает, что sizeof(buffer) количество байтов, начиная с &buffer инициализируются.

  • memset: Переменное количество аргументов.

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

    void* my_memset(void*, int, size_t, ...)
    Чтобы сопоставить функцию с memset function, использовать следующее отображение:
    <function name="my_memset" std="memset">
        <mapping std_arg="1" arg="1"></mapping>
        <mapping std_arg="2" arg="2"></mapping>
        <mapping std_arg="3" arg="3"></mapping>
    </function>

Эффект отображения на точность

Эти примеры показывают результат отображения определенных функций к стандартным функциям:

  • my_acosacos:

    Если вы используете отображение, User assertion чек становится зеленым. Верификация принимает, что возврат значение my_acos равен 0.

    • Перед отображением:

      double x = my_acos(1.0);  
      assert(x <= 2.0);

    • Спецификация отображения:

      <function name="my_acos" std="acos">
      </function>

    • После отображения:

      double x = my_acos(1.0);  
      assert(x <= 2.0);

  • my_sqrtsqrt:

    Если вы используете отображение, Invalid use of standard library routine проверка становится красной. В противном случае верификация не проверяет, является ли аргумент my_sqrt неотрицательная.

    • Перед отображением:

      res = my_sqrt(-1.0);

    • Спецификация отображения:

      <function name="my_sqrt" std="sqrt"> 
      </function>

    • После отображения:

      res = my_sqrt(-1.0);

  • my_lookup_table (аргумент 2) →<reservedrangesplaceholder0> (аргумент 1):

    Если вы используете отображение, User assertion чек становится зеленым. Верификация принимает, что возврат значение my_lookup_table находится в области значений массива интерполяционной таблицы table.

    • Перед отображением:

      double table[3] = {1.1, 2.2, 3.3}
      .
      .
      double res = my_lookup_table(u, table, bp);
      assert(res >= 1.1 && res <= 3.3);

    • Спецификация отображения:

      <function name="my_lookup_table" std="__ps_lookup_table_clip">
          <mapping std_arg="1" arg="2"></mapping>
      </function>

    • После отображения:

      double table[3] = {1.1, 2.2, 3.3}
      .
      .
      res_real = my_lookup_table(u, table9, bp);
      assert(res_real >= 1.1 && res_real <= 3.3);

  • my_meminit__ps_meminit:

    Если вы используете отображение, Non-initialized local variable чек становится зеленым. Эта верификация принимает, что все поля структуры x инициализируются с допустимыми значениями.

    • Перед отображением:

      struct X {
        int field1 ;
        int field2 ;
      };
      .
      .
      struct X x;
      my_meminit(&x, sizeof(struct X));
      return x.field1;

    • Спецификация отображения:

      <function name="my_meminit" std="__ps_meminit">
           <mapping std_arg="1" arg="1"></mapping>
           <mapping std_arg="2" arg="2"></mapping>
      </function>

    • После отображения:

      struct X {
        int field1 ;
        int field2 ;
      };
      .
      .
      struct X x;
      my_meminit(&x, sizeof(struct X));
      return x.field1;

  • my_meminit__ps_meminit:

    Если вы используете отображение, Non-initialized local variable проверка становится красной. Эта верификация принимает, что только поле field1 структуры x инициализируется с допустимыми значениями.

    • Перед отображением:

      struct X {
        int field1 ;
        int field2 ;
      };
      .
      .
      struct X x;
      my_meminit(&x, sizeof(int));
      return x.field2;

    • Спецификация отображения:

      <function name="my_meminit" std="__ps_meminit">
      </function>

    • После отображения:

      struct X {
        int field1 ;
        int field2 ;
      };
      .
      .
      struct X x;
      my_meminit(&x, sizeof(int));
      return x.field2;

Введенный в R2016b