Exponenta Banner

Допущения о упорных функциях

Функции верификации заглушки, которые не определены в исходном коде или которые вы принимаете решение заглушить. Для упрямой функции:

  • Верификация делает определенные предположения о функции возврата значении и других побочных эффектах функции.

    Можно точно настроить допущения, задав ограничения.

  • Если верификация существует, тело функции игнорируется. Операции в теле функции не проверяются на ошибки времени выполнения.

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

Для заглушки функций можно использовать следующие опции:

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

В верификацию сделаны следующие предположения о аргументах упрямых функций.

Функция Возврата значение

Предположения

Эта верификация принимает, что:

  • Переменная, возвращенная функцией, принимает полную область значений значений, разрешенных ее типом данных.

    Если функция возвращает enum переменная, значение переменных находится в области значений перечисления. Для образца, если enum тип принимает значения {0,5, -1,32}, и упрямая функция имеет этот возврат тип, верификация принимает, что функция возвратов значения в область значений -1.. 32.

  • Если функция возвращает указатель, указатель не является NULL и безопасен для дереференции. Указатель не указывает на динамически выделенную память или другую переменную в вашем коде.

  • 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) (Визуальная студия®) или __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 */ 
}
#endif
    Определите макрос POLYSPACE при помощи опции Preprocessor definitions (-D). Вместо фактического определения функции верификации использует заглушку.

  • Если функция возвращает переменную, можно указать, что указатель может быть NULL.

Аргументы функции, которые являются указателями

Предположения

Эта верификация принимает, что:

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

    Например, в этом примере верификация принимает, что упрямая функция stubbedFunc записывает любое возможное значение в val. Поэтому значение оранжевого цвета.

    void stubbedFunc(int*);

void main() {
    int val=0, *ptr=&val;
    stubbedFunc(ptr);
    assert(val==0);
}

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

    В коде С++ только представители данных первого уровня структуры могут быть записаны через указатель на структуру. Например, в этом примере анализ имеет знания о том, что pb->j указывает на, но не на что pb->pa->i указывает на. Итак, после вызова на Foo, b.j появляется как инициализированный, но a.i не инициализирован.

    struct A {
   int i;
};
 
struct B {
   A* pa;
   int j;
};
 
void Foo(B*);
 
void main() {
    A a;
    B b;
    b.pa = &a;
    Foo(&b); 
    int var1 = b.j;
    int var2 = a.i;
}

  • Если аргумент является указателем на другой указатель, функция может записать любое значение в объект, на который указывает второй указатель (только код С). Это предположение продолжается до произвольных глубин иерархии указателей.

    Например, предположим, что указатель **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 */
}
#endif
Определите макрос POLYSPACE при помощи опции Preprocessor definitions (-D). Вместо фактического определения функции верификации использует заглушку.

Глобальные переменные

Предположения

Эта верификация принимает, что заглушка функции не изменяет глобальные переменные.

Как изменить допущения

Чтобы смоделировать операции записи на глобальную переменную, запишите заглушку функции.

Для образца неопределенная функция имеет прототип:

void func(void);
Предположим, вы знаете, что функция записывает значение 0 или 1 в глобальную переменную 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 */
}
#endif
Определите макрос POLYSPACE использование опции Preprocessor definitions (-D). Вместо фактического определения функции верификации использует заглушку.

Документация Polyspace Code Prover

Поддержка