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