Эта тема показывает, как создать средства проверки для ваших пользовательских библиотечных функций путем отображения их с эквивалентными функциями от Стандартной Библиотеки.
Если вы идентифицируете средство проверки Средства поиска Ошибки, которое применяется к Стандартной Библиотечной функции и может быть расширено к вашей пользовательской библиотечной функции, использовать этот метод.
Например, вы можете задать математическую функцию, которая имеет ту же область как Стандартная математическая функция Библиотеки. Если Средство поиска Ошибки проверяет на доменные ошибки при использовании Стандартной Библиотечной функции, можно выполнить те же проверки для эквивалентной пользовательской функции.
Предположим, что вы задаете функциональный 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 реализация не точна, Средство поиска Ошибки не может обнаружить проблему. Однако функция имеет ту же область как Стандартная Библиотечная функция 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.
Следующие средства проверки могут быть расширены таким образом: