Функции тупиков верификации, которые не заданы в вашем исходном коде или что вы принимаете решение заблокировать. Для заблокированной функции:
Верификация делает определенные предположения о функциональном возвращаемом значении и других побочных эффектах функции.
Можно подстроить предположения путем определения ограничений.
Верификация игнорирует тело функции, если это существует. Операции в теле функции не проверяются на ошибки времени выполнения.
Если верификация тела функции неточна и вызывает много оранжевых проверок, когда вы вызываете функцию, можно принять решение заблокировать функцию. Чтобы сократить количество оранжевых проверок, вы блокируете функцию, и затем ограничиваете возвращаемое значение функции и задаете другие побочные эффекты.
К интерфейсным функциям можно использовать эти опции:
Functions to stub (-functions-to-stub): Задайте функции, которые вы хотите заблокированный.
Generate stubs for Embedded Coder lookup tables (-stub-embedded-coder-lookup-table-functions): Интерфейсные функции, которые содержат интерполяционные таблицы в коде, сгенерированном из моделей с помощью Embedded Coder®.
-function-behavior-specifications: Интерфейсные функции, которые соответствуют стандартной функции, которую распознает Polyspace®.
Если вы используете право преимущественной покупки, чтобы заблокировать функцию, вы ограничиваете функциональное возвращаемое значение и моделируете другие побочные эффекты путем определения ограничений. Если вы хотите задать ограничения, более мелкомодульные, чем те доступные через ограничительный интерфейс спецификации Polyspace, задайте свои собственные тупики. Если вы используете другие опции для интерфейсных функций, само программное обеспечение ограничивает функциональное возвращаемое значение и моделирует его побочные эффекты соответственно.
Верификация делает следующие предположения об аргументах заблокированных функций.
Верификация принимает что:
Переменная, возвращенная функцией, берет полный спектр значений, позволенных его типом данных.
Если функция возвращает переменную enum, значение переменных находится в области значений перечисления. Например, если тип enum принимает, значения {0,5,-1,32} и заблокированная функция имеют тот тип возврата, верификация принимает, что функция возвращает значения в области значений-1.. 32.
Если функция возвращает указатель, указатель не является ПУСТЫМ и безопасным разыменовать. Указатель не указывает на динамически выделенную память или другую переменную в вашем коде.
C++ определенные предположения: оператор new возвращает выделенную память. Операторы, такие как operator=, operator+=, operator-- (снабженная префиксом версия) или operator<< возвращаются:
Ссылка на *this, если оператор является частью определения класса.
Например, если оператор задан как:
class X {
X& operator=(const X& arg) ;
};
*this (объект, который вызывает оператор). Объект, который вызывает оператор или его элементы данных, имеет полный спектр значений, позволенных их типом.Первый аргумент, если оператор не является частью определения класса.
Например, если оператор задан как:
X& operator+=(X& arg1, const X& arg2) ;
arg1. Объект, который arg1 отсылает к или его элементы данных, имеет полный спектр значений, позволенных их типом. Функции, объявленные с __declspec(no_return) (Визуальный Studio®) или __attribute__ ((noreturn)) (GCC), не возвращаются.
Можно изменить предположения по умолчанию о функциональном возвращаемом значении.
Если функция возвращает неуказательную переменную, можно ограничить ее область значений. Используйте опцию Constraint setup (-data-range-specifications).
Через ограничительный интерфейс спецификации можно задать абсолютную область значений [min..max]
Например, неопределенная функция имеет прототип:
int func(int ll, int ul);
int func(int ll, int ul) {
int ret;
assert(ret>=ll && ret <=ul);
return ret;
}Если определение func существует в вашем коде, и вы хотите заменить определение, потому что верификация тела функции неточна, встройте фактическое определение и тупик в операторе #ifdef:
#ifdef POLYSPACE
int func(int ll, int ul) {
int ret;
assert(ret>=ll && ret <=ul);
return ret;
}
#else
int func(int ll, int ul) {
/*Your function body */
}
#endifPOLYSPACE при помощи опции Preprocessor definitions (-D). Верификация использует ваш тупик вместо фактического функционального определения.Если функция возвращает переменную указателя, можно указать, что указателем может быть NULL.
Чтобы задать это предположение для всех заблокированных функций, используйте опцию Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe).
Чтобы задать это предположение для определенных заблокированных функций, используйте опцию Constraint setup (-data-range-specifications).
Верификация принимает что:
Если аргумент является указателем, функция может записать любое значение в объект, на который указывает указатель. Область значений значений ограничивается одним только типом данных аргумента.
Если резкий объект является ранее неинициализированным, функция может оставить объект неинициализированным.
Например, в этом примере, верификация принимает, что заблокированный функциональный stubbedFunc пишет любое возможное значение в val. Поэтому утверждение является оранжевым.
void stubbedFunc(int*);
void main() {
int val=0, *ptr=&val;
stubbedFunc(ptr);
assert(val==0);
}Если аргумент является указателем на структуру, функция может записать любое значение в поля структуры. Область значений значений ограничивается только по условию тип полей.
Если резкая структура является ранее неинициализированной или частично инициализированная, функция может оставить объект неинициализированным или частично инициализированным.
Если аргумент является указателем на другой указатель, функция может записать любое значение в объект, который второй указатель указывает на (Только код С). Это предположение продолжается к произвольным глубинам иерархии указателя.
Например, предположите, что указатель, который **pp указывает на другой указатель *p, который указывает на переменную int var. Если заблокированная функция берет **p в качестве аргумента, верификация принимает, что, следуя за вызовом функции, var имеет любое значение int. *p может указать на где угодно в выделенной памяти или может указать на var, но не указывает на другую переменную в коде.
Если аргумент является указателем функции, функция, на которую он указывает, вызвана (Только код С).
Например, в этом примере, заблокированный функциональный stubbedFunc берет указатель функции funcPtr в качестве аргумента. funcPtr указывает на func, который называется, когда вы вызываете stubbedFunc.
typedef int (*typeFuncPtr) (int);
int func(int x){
return x;
}
int stubbedFunc(typeFuncPtr);
void main() {
typeFuncPtr funcPtr = (typeFuncPtr)(&func);
int result = stubbedFunc(funcPtr);
}Можно ограничить область значений аргумента, который передается ссылкой. Используйте опцию Constraint setup (-data-range-specifications).
Через ограничительный интерфейс спецификации можно задать абсолютную область значений [min..max]
Например, неопределенная функция имеет прототип:
void func(int *x, int ll, int ul);
x, находится между вторым и третьими аргументами. Однако программное обеспечение принимает полный спектр для значения *x, потому что функция не задана. Чтобы смоделировать поведение, что вы хотите и уменьшаете оранжевые проверки от неточности, запишите функциональный тупик можно следующим образом:void func(int *x, int ll, int ul) {
assert(*x>=ll && *x <=ul);
}Если определение func существует в вашем коде, и вы хотите заменить определение, потому что верификация тела функции неточна, встройте фактическое определение и тупик в операторе #ifdef:
#ifdef POLYSPACE
void func(int *x, int ll, int ul) {
assert(*x>=ll && *x <=ul);
}
#else
void func(int *x, int ll, int ul) {
/* Your function body */
}
#endifPOLYSPACE при помощи опции Preprocessor definitions (-D). Верификация использует ваш тупик вместо фактического функционального определения.Верификация принимает, что функциональный тупик не изменяет глобальные переменные.
Чтобы смоделировать операции записи на глобальной переменной, запишите функциональный тупик.
Например, неопределенная функция имеет прототип:
void func(void);
glob. Чтобы смоделировать поведение, которое вы хотите, запишите функциональный тупик можно следующим образом:void func(void) {
volatile int randomVal;
if(randomVal)
glob = 0;
else
glob = 1;
}Если определение func существует в вашем коде, и вы хотите заменить определение, потому что верификация тела функции неточна, встройте фактическое определение и тупик в операторе #ifdef можно следующим образом:
#ifdef POLYSPACE
void func(void) {
volatile int randomVal;
if(randomVal)
glob = 0;
else
glob = 1;
}
#else
void func(void) {
/* Your function body */
}
#endifPOLYSPACE с помощью опции Preprocessor definitions (-D). Верификация использует ваш тупик вместо фактического функционального определения.