Объектно-ориентированные языки, такие как 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 }Класс анализатор вызывает конструктора и затем методы в любом порядке много раз.
Верификация этого класса подсвечивает две проблемы:
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 только путем обеспечения его кода программному обеспечению. Это соответствует предыдущему разделу “Simple Class” в этой главе.
Можно анализировать класс B класс путем обеспечения его коду и классу A объявление. В этом случае, A код будет заблокирован автоматически программным обеспечением.
Можно анализировать класс B класс путем обеспечения B и A коды (объявление и определение). Это находится на одном уровне “сначала интегрирования” верификация. Класс анализатор не вызовет A методы. В этом случае цель состоит в том, чтобы найти ошибки только в классе B код.
Можно анализировать класс C путем обеспечения C код, B объявление класса и A объявление класса. В этом случае, A и B коды будут заблокированы автоматически.
Можно анализировать класс C путем обеспечения AB и C код для верификации интегрирования. Класс анализатор вызовет весь C методы, но не унаследованные методы от B и A. Цель состоит в том, чтобы найти только дефекты в классе C.
В этих случаях нет никакой потребности предоставить код класса D для анализа AB и классы C, пока они не используют класс (например, тип элемента) или нуждаться в нем (например, наследоваться).
Рассмотрите следующие классы:
A и B базовые классы C.
В этом случае программное обеспечение Polyspace позволяет вам запускать следующие верификации:
Можно анализировать классы A и B отдельно только путем обеспечения их кодов программному обеспечению. Это соответствует предыдущему разделу “Simple Class” в этой главе.
Можно анализировать класс C путем предоставления его коду A и B объявления. A и B методы будут заблокированы автоматически.
Можно анализировать класс C путем обеспечения AB и C коды для верификации интегрирования. Класс анализатор вызовет все методы C, но не унаследованные методы от A и B. Цель состоит в том, чтобы найти ошибки только в классе C.
Рассмотрите следующие классы:
B и C классы фактически наследовали класс
B и C базовые классы D.
ABC и D может анализироваться таким же образом как описано в предыдущем разделе “Абстрактные классы”.
Виртуальное наследование не оказывает влияния на способ использовать класс анализатор.
Рассмотрите C класс, который наследовался A и B классы и имеют элементы объекта AA и BB классы.
Верификация интегрирования класса состоит из проверки класса C и обеспечение кодов для AB, AA и BB. Если некоторые определения будут отсутствовать, программное обеспечение автоматически заблокирует их.