Объектно-ориентированные языки, такие как C++, предназначены для переиспользуемости. При разработке кода на таком языке вы не обязательно знаете все контексты, в которых развернут класс. Класс или семейство классов безопасно для повторного использования, если они не имеют дефектов для всех возможных контекстов.
Чтобы сделать ваши классы безопасными для всех возможных контекстов, выполните верификацию робастности и удалите как можно больше ошибки времени выполнения.
Polyspace® По умолчанию Code Prover™ выполняет верификацию робастности. Если вы предоставляете программному обеспечению определение класса вместе с определением методов класса, программное обеспечение моделирует все использования класса. Если некоторые определения методов отсутствуют, программа автоматически заглушает их.
Программа проверяет каждый конструктор путем создания объекта с помощью конструктора. Если конструктор не существует, программное обеспечение использует конструктор по умолчанию.
Программное обеспечение проверяет общие, статические и защищенные методы классов тех объектов, принимая, что:
Методы могут быть вызваны в произвольном порядке.
Параметры метода могут иметь любое значение в область значений, допустимой их типом данных.
Чтобы выполнить эту верификацию, по умолчанию она генерирует main функция, которая вызывает методы, которые не вызываются в другом месте кода. Если необходимо проверить все методы для всех контекстов, измените это поведение так, чтобы сгенерированные main Вызовы все публичные и защищенные методы вместо просто незакрытых таковых. Для получения дополнительной информации смотрите Functions to call within the specified classes (-class-analyzer-calls).
Программа вызывает деструктор этих объектов (если они существуют) и проверяет их.
При проверке классов Polyspace делает определенные предположения.
| Кодовая Конструкция | Предположение |
|---|---|
| Глобальная переменная | Если не инициализировано явно, в каждом методе глобальные переменные могут иметь любое значение, разрешенное их типом. Для образца в следующем коде Polyspace принимает, что extern int fround(float fx);
// global variables
int globvar1;
int globvar2 = 100;
class Location
{
private:
int x;
public:
Location(int intx = 0) {
x = intx;
};
void setx(int intx) {
x = intx;
};
void fsetx(float fx) {
int tx = fround(fx);
if (tx / globvar1 != 0)
{
tx = tx / globvar2;
setx(tx);
}
};
}; |
| Классы с неопределенными конструкторами | Представители классов могут быть неинициализированы. В следующем примере Polyspace принимает, что class OtherClass
{
protected:
int x;
public:
OtherClass (int intx);
int getMember(void) {
return x;
};
};
class MyClass
{
OtherClass m_loc;
public:
MyClass(int intx) : m_loc(0) {};
void show(void) {
int wx, wl;
wx = m_loc.getMember();
wl = wx + 2;
};
};
|
Примите во внимание следующий класс:
Stack.h
#define MAXARRAY 100
class stack
{
int array[MAXARRAY];
long toparray;
public:
int top (void);
bool isempty (void);
bool push (int newval);
void pop (void);
stack ();
};
stack.cpp
1 #include "stack.h"
2
3 stack::stack ()
4 {
5 toparray = -1;
6 for (int i = 0 ; i < MAXARRAY; i++)
7 array[i] = 0;
8 }
9
10 int stack::top (void)
11 {
12 int i = toparray;
13 return (array[i]);
14 }
15
16 bool stack::isempty (void)
17 {
18 if (toparray >= 0)
19 return false;
20 else
21 return true;
22 }
23
24 bool stack::push (int newvalue)
25 {
26 if (toparray < MAXARRAY)
27 {
28 array[++toparray] = newvalue;
29 return true;
30 }
31
32 return false;
33 }
34
35 void stack::pop (void)
36 {
37 if (toparray >= 0)
38 toparray--;
39 }Анализатор классов вызывает конструктор, а затем методы в любом порядке много раз.
В верификацию этого класса выделены две задачи:
The stack::push метод может записывать после последнего элемента массива, получая в результате оранжевую проверку OBAI в линии 28.
Если вызывается перед push, а stack::top метод получит доступ к элементу -1, что приведет к проверкам OBAI и NIV в линии 13.
Устранение этих проблем устранит ошибки времени выполнения в этом классе.
Класс шаблона позволяет вам создавать класс без явного знания типа данных, которым обрабатывают операции класса. Polyspace не может проверить класс шаблона непосредственно. Программа может проверить только определенный образец класса шаблона. Чтобы проверить класс шаблона:
Создайте явный образец класса.
Задайте typedef образца и предусмотреть, что typedef для верификации.
В следующем примере calc - класс шаблона, который может обрабатывать любой тип данных через идентификатор myType.
template <class myType> class calc
{
public:
myType multiply(myType x, myType y);
myType add(myType x, myType y);
};
template <class myType> myType calc<myType>::multiply(myType x,myType y)
{
return x*y;
}
template <class myType> myType calc<myType>::add(myType x, myType y)
{
return x+y;
}
Чтобы проверить этот класс:
Добавьте следующий код к своему проекту Polyspace.
template class calc<int>; typedef calc<int> my_template;
Обеспечивайте my_template как аргумент опции Class. См. Class (-class-analyzer).
В реальном мире образец абстрактного класса не может быть создан, поэтому его нельзя анализировать. Однако легко установить верификацию путем удаления чистых заявлений. Для примера это может быть достигнуто посредством абстрактного класса изменения определения:
void abstract_func () = 0; by void abstract_func ();
Если для верификации предусмотрен абстрактный класс, программное обеспечение автоматически сделает изменение и виртуальную чистую функцию (abstract_func в приведенном выше примере) будет проигнорировано во время верификации абстрактного класса.
Это означает, что из сгенерированного основного вызова не будет выполняться, поэтому функция полностью игнорируется. Более того, если функция вызывается другой, чистая виртуальная функция будет упорна, и при вызове будет установлена оранжевая проверка с сообщением «вызов виртуальной функции [f] может быть чистым».
Примите во внимание следующие классы:
A является абстрактным классом
B является простым классом.
A и B являются базовыми классами C.
C не является абстрактным классом.
Так как невозможно создать объект класса A, этот класс не может быть проанализирован отдельно от других классов. Поэтому вам не разрешено задавать класс A для анализатора классов Polyspace. Конечно, классовые C могут быть проанализированы так же, как и в предыдущем разделе «Множественное наследование».
Если класс определяет статические методы, он вызывается в сгенерированном основном как классический.
Когда функция не задана в производном классе, даже если она видна, поскольку унаследована от класса отца, она не вызывается в сгенерированном основном. В приведенном ниже примере класс Point определяется из класса Location:
class Location
{
protected:
int x;
int y;
Location (int intx, int inty);
public:
int getx(void) {return x;};
int gety(void) {return y;};
};
class Point : public Location
{
protected:
bool visible;
public :
Point(int intx, int inty) : Location (intx, inty)
{
visible = false;
};
void show(void) { visible = true;};
void hide(void) { visible = false;};
bool isvisible(void) {return visible;};
};Хотя два метода Location::getx и Location::gety видны для производных классов, сгенерированная основная не включает эти методы при анализе класса Point.
Унаследованные представители считаются изменчивыми, если они не инициализированы явно в конструкторах отца. В приведенном выше примере два представителей Location::x и Location::y будет считаться летучим. Если мы анализируем вышеописанный пример в его текущем состоянии, метод Location:: Location(constructor) будет упрямым.
Примите во внимание следующие классы:
A является базовым классом B и D.
B является базовым классом C.
В таком случае программное обеспечение Polyspace позволяет запускать следующие верификации:
Можно анализировать A классов просто предоставив свой код программному обеспечению. Это соответствует предыдущему разделу «Простой класс» в этой главе.
Можно анализировать B классов класс путем предоставления его кода и A класса декларация. В этом случае A код будет автоматически утоплен программным обеспечением.
Можно анализировать B классов класс путем предоставления B и A коды (объявление и определение). Это верификация «первого уровня интегрирования». Анализатор классов не будет вызывать A методы. В этом случае цель состоит в том, чтобы найти ошибки только в классе B код.
Можно анализировать C классов путем предоставления C код, B объявления классов и A объявление класса. В этом случае A и B коды будут стерты автоматически.
Можно анализировать C классов путем предоставления A, B и C код для верификации интегрирования. Анализатор классов вызовет все C методы, но не унаследованные методы от B и A. Цель состоит в том, чтобы найти только дефекты в C классов.
В этих случаях нет необходимости предоставлять код класса D для анализа A, B и классы C, пока они не используют класс (например, тип представителя) или не нуждаются в нем (например, наследование).
Примите во внимание следующие классы:
A и B являются базовыми классами C.
В этом случае программное обеспечение Polyspace позволяет запускать следующие верификации:
Можно анализировать классы A и B отдельно просто предоставляя свои коды программному обеспечению. Это соответствует предыдущему разделу «Простой класс» в этой главе.
Можно анализировать C классов путем предоставления своего кода с A и B декларации. A и B методы будут стерты автоматически.
Можно анализировать C классов путем предоставления A, B и C коды для интегрирования верификации. Анализатор классов вызовет все методы C, но не наследуемые методы от A B. Цель состоит в том, чтобы найти ошибки только в классовых C.
Примите во внимание следующие классы:
B и C классы фактически наследуют класс A
B и C являются базовыми классами D.
A, B, C и D могут быть проанализированы так же, как описано в предыдущем разделе «Абстрактные классы».
Виртуальное наследование не влияет на способ использования анализатора классов.
Рассмотрим C класс, который наследует от A и B Классы и имеют представителей объекта AA и BB классы.
Класс интегрирования верификации состоит из проверки C классов и предоставление кодов для A, B, AA и BB. Если некоторые определения отсутствуют, программное обеспечение автоматически заглушит их.