В этом разделе показано, как создать шашки для пользовательских библиотечных функций путем сопоставления их с эквивалентными функциями из стандартной библиотеки.
Если вы идентифицируете проверку Bug Finder, которая применяется к функции Standard Library и может быть расширена на пользовательскую функцию библиотеки, используйте этот метод.
Например, можно задать математическую функцию, которая имеет ту же область, что и математическая функция Стандартной библиотеки. Если Bug Finder проверяет ошибки области при использовании функции Standard Library, можно выполнить те же проверки эквивалентной пользовательской функции.
Предположим, что вы задаете функцию 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 может не обнаружить проблему. Однако функция имеет ту же область, что и функция Standard Library acos. Можно продлить чекер Invalid use of standard library floating point routine который обнаруживает ошибки области в использовании acos обнаружение тех же видов ошибок с acos32.Если ваша пользовательская функция не имеет ограниченной области, но возвращает значения в ограниченной области значений, можно по-прежнему сопоставить функцию с эквивалентной функцией Standard Library (если она существует) для получения более точных результатов на других шашках. Например, можно сопоставить функцию cos32 который возвращает значения в области значений [-1,1] в функцию Standard Library cos.
Можно расширить функции проверки из стандартной библиотеки, сопоставив эти функции с пользовательскими функциями библиотеки. Например, в предыдущем примере можно сопоставить функцию acos32 функции «Стандартная библиотека» acos.
Чтобы выполнить отображение:
Перечислите каждое отображение в XML- файл в определенном синтаксисе.
Скопируйте файл шаблона code-behavior-specifications-template.xml из папки polyspaceroot\ polyspace\verifier\cxx
<function name="acos32" std="acos"> </function>
Укажите этот XML- файл в качестве аргумента для опции -code-behavior-specifications.
Таким образом могут быть расширены следующие шашки: