Эта тема показывает, как создать средства проверки для ваших пользовательских библиотечных функций путем отображения их с эквивалентными функциями от Стандартной Библиотеки.
Если вы идентифицируете средство проверки Bug Finder, которое применяется к Стандартной Библиотечной функции и может быть расширено к вашей пользовательской библиотечной функции, использовать этот метод.
Например, вы можете задать математическую функцию, которая имеет ту же область как Стандартная математическая функция Библиотеки. Если Bug Finder проверяет на доменные ошибки при использовании Стандартной Библиотечной функции, можно выполнить те же проверки для эквивалентной пользовательской функции.
Предположим, что вы задаете функциональный acos32
это ожидает значения в области значений [-1,1]. Вы можете хотеть обнаружить, если аргумент функции выходит за пределы этой области значений во время выполнения, например, в этом фрагменте кода:
#include<math.h> #include<float.h> double acos32(double); const int periodicity = 1.0; int isItPeriodic() { return(abs(func(0.5) - func(0.5 + periodicity)) < DBL_MIN); } double func(double val) { return acos32(val); }
acos32
находится вне его позволенной области. Если вы не обеспечиваете реализацию acos32
или если анализ acos32
реализация не точна, Bug Finder не может обнаружить проблему. Однако функция имеет ту же область как Стандартная Библиотечная функция acos
. Можно расширить средство проверки Invalid use of standard library floating point routine
это обнаруживает доменные ошибки в использовании acos
обнаружить те же виды ошибок с acos32
.Если ваша пользовательская функция не имеет ограниченной области, но возвращает значения в ограниченной области значений, можно все еще сопоставить функцию с эквивалентной Стандартной Библиотечной функцией (если вы существуете) для более точных результатов на других средствах проверки. Например, можно сопоставить функциональный cos32
это возвращает значения в области значений [-1,1] к Стандартной Библиотечной функции cos
.
Можно расширить средства проверки на функциях от Стандартной Библиотеки путем отображения тех функций с пользовательскими библиотечными функциями. Например, в предыдущем примере, можно сопоставить функциональный acos32
к Стандартной Библиотечной функции acos
.
Выполнять отображение:
Перечислите каждое отображение в XML-файле в определенном синтаксисе.
Скопируйте файл шаблона code-behavior-specifications-template.xml
от папки
к перезаписываемому местоположению и изменяют файл. Введите отображение в файл с помощью следующего синтаксиса после существующих подобных записей:polyspaceroot
\polyspace\verifier\cxx
<function name="acos32" std="acos"> </function>
Задайте этот XML-файл в качестве аргумента для опции -code-behavior-specifications
.
Следующие средства проверки могут быть расширены таким образом: