-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 в качестве Вас Расширения кода в ИДАХ, введите эту опцию в файл опций анализа. Смотрите файл опций.

Используя опцию для улучшения точности

Синтаксис XML: <имя функции = "custom_function"станд. = "std_function"> </функция>

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

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

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

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

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

    Например, если вы сопоставляете свой функциональный acos32 к стандартной функции acosInvalid 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.

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

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

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

Синтаксис XML: <имя функции = "custom_function"станд. = "std_function"> </функция>

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

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

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

Используя опцию для помещения в черный список функций

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

Синтаксис XML:

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

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

Смотрите флаг или небезопасные функции устаревшие Используя средства проверки Bug Finder.

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

Синтаксис 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: Максимальные уровни включения позволили использовать, включают файлы.

    • 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: Количество символов, чтобы выдержать сравнение для внутренних идентификаторов.

Примеры

Примеры в следующих разделах относятся к анализу Программы автоматического доказательства Кода. Для примеров 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. Задайте местоположение файла для верификации:

    • Программа автоматического доказательства кода:

      polyspace-code-prover -code-behavior-specifications "C:\Polyspace_projects\Common\Config_files\code-behavior-specifications-template.xml"
    • Сервер программы автоматического доказательства кода:

      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 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) →__ps_lookup_table_clip (аргумент 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;

Смотрите также

Введенный в R2017b