Verify C++ Classes

Verification of Classes

Object-oriented languages such as C++ are designed for reusability. When developing code in such a language, you do not necessarily know every contexts in which the class is deployed. A class or a class family is safe for reuse if it free of defects for all possible contexts.

To make your classes safe against all possible contexts, perform a robustness verification and remove as many run-time errors as possible.

Polyspace^® Code Prover™ performs a robustness verification by default. If you provide the software the class definition together with the definition of the class methods, the software simulates all uses of the class. If some of the method definitions are missing, the software automatically stubs them.

1. The software verifies each constructor by creating an object using the constructor. If a constructor does not exist, the software uses the default constructor.

2. The software verifies the public, static and protected class methods of those objects assuming that:

   • The methods can be called in arbitrary order.

   • The method parameters can have any value in the range allowed by their data type.

   To perform this verification, by default, it generates a main function that calls the methods that are not called elsewhere in the code. If you want all your methods to be verified for all contexts, modify this behavior so that the generated main calls all public and protected methods instead of just the uncalled ones. For more information, see Functions to call within the specified classes (-class-analyzer-calls).

3. The software calls the destructor of those objects (if they exist) and verifies them.

When verifying classes, Polyspace makes certain assumptions.

Code Construct	Assumption
Global variable	Unless explicitly initialized, in each method, global variables can have any value allowed by their type. For instance, in the following code, Polyspace assumes that globvar1 can have any value allowed by its type. Therefore, an orange Division by zero appears on the division by globvar1. However, because globvar2 is explicitly initialized, the Division by zero check on division by globvar2 is green. 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); } }; };
Classes with undefined constructors	The members of the classes can be non-initialized. In the following example, Polyspace assumes that m_loc.x can be non-initialized. Therefore, an orange Non-initialized variable error appears on x in the getMember method. Following the check, Polyspace assumes that the variable can have any value allowed by its type. Therefore, an orange Overflow appears on the addition operation in the show method. 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; }; };

Methods and Class Specifics

• Simple Class

• Template Classes

• Abstract Classes

• Static Classes

• Inherited Classes

• Simple Inheritance

• Multiple Inheritance

• Virtual Inheritance

• Class Integration

Simple Class

Consider the following class:

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 class analyzer calls the constructor and then the methods in any order many times.

The verification of this class highlights two problems:

• The stack::push method may write after the last element of the array, resulting in the OBAI orange check at line 28.

• If called before push, the stack::top method will access element -1, resulting in the OBAI and NIV checks at line 13.

Fixing these problems will eliminate run-time errors in this class.

Template Classes

A template class allows you to create a class without explicit knowledge of the data type that the class operations handle. Polyspace cannot verify a template class directly. The software can only verify a specific instance of the template class. To verify a template class:

1. Create an explicit instance of the class.

2. Define a typedef of the instance and provide that typedef for verification.

In the following example, calc is a template class that can handle any data type through the identifier 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;
}

To verify this class:

1. Add the following code to your Polyspace project.

   template class calc<int>;
   typedef calc<int> my_template;

2. Provide my_template as argument of the option Class. See Class (-class-analyzer) (Polyspace Code Prover).

Abstract Classes

In the real world, an instance of an abstract class cannot be created, so it cannot be analyzed. However, it is easy to establish a verification by removing the pure declarations. For example, this can be accomplished via an abstract class definition change:

void abstract_func () = 0; by void abstract_func ();

If an abstract class is provided for verification, the software will make the change automatically and the virtual pure function (abstract_func in the example above) will then be ignored during the verification of the abstract class.

This means that no call will be made from the generated main, so the function is completely ignored. Moreover, if the function is called by another one, the pure virtual function will be stubbed and an orange check will be placed on the call with the message “call of virtual function [f] may be pure.”

Consider the following classes:

A is an abstract class

B is a simple class.

A and B are base classes of C.

C is not an abstract class.

As it is not possible to create an object of class A, this class cannot be analyzed separately from other classes. Therefore, you are not allowed to specify class A to the Polyspace class analyzer. Of course, class C can be analyzed in the same way as in the previous section “Multiple Inheritance.”

Static Classes

If a class defines a static methods, it is called in the generated main as a classical one.

Inherited Classes

When a function is not defined in a derived class, even if it is visible because it is inherited from a father's class, it is not called in the generated main. In the example below, the class Point is derived from the class 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;};
};

Although the two methods Location::getx and Location::gety are visible for derived classes, the generated main does not include these methods when analyzing the class Point.

Inherited members are considered to be volatile if they are not explicitly initialized in the father's constructors. In the example above, the two members Location::x and Location::y will be considered volatile. If we analyze the above example in its current state, the method Location:: Location(constructor) will be stubbed.

Simple Inheritance

Consider the following classes:

A is the base class of B and D.

B is the base class of C.

In a case such a this, Polyspace software allows you to run the following verifications:

1. You can analyze class A just by providing its code to the software. This corresponds to the previous “Simple Class” section in this chapter.

2. You can analyze class B class by providing its code and the class A declaration. In this case, A code will be stubbed automatically by the software.

3. You can analyze class B class by providing B and A codes (declaration and definition). This is a “first level of integration” verification. The class analyzer will not call A methods. In this case, the objective is to find bugs only in the class B code.

4. You can analyze class C by providing the C code, the B class declaration and the A class declaration. In this case, A and B codes will be stubbed automatically.

5. You can analyze class C by providing the A, B and C code for an integration verification. The class analyzer will call all the C methods but not inherited methods from B and A. The objective is to find only defects in class C.

In these cases, there is no need to provide D class code for analyzing A, B and C classes as long as they do not use the class (e.g., member type) or need it (e.g., inherit).

Multiple Inheritance

Consider the following classes:

A and B are base classes of C.

In this case, Polyspace software allows you to run the following verifications:

1. You can analyze classes A and B separately just by providing their codes to the software. This corresponds to the previous “Simple Class” section in this chapter.

2. You can analyze class C by providing its code with A and B declarations. A and B methods will be stubbed automatically.

3. You can analyze class C by providing A, B and C codes for an integration verification. The class analyzer will call all the C methods but not inherited methods from A and B. The objective is to find bugs only in class C.

 

Virtual Inheritance

Consider the following classes:

B and C classes virtually inherit the A class

B and C are base classes of D.

A, B, C and D can be analyzed in the same way as described in the previous section “Abstract Classes.”

Virtual inheritance has no impact on the way of using the class analyzer.

Class Integration

Consider a C class that inherits from A and B classes and has object members of AA and BB classes.

A class integration verification consists of verifying class C and providing the codes for A, B, AA and BB. If some definitions are missing, the software will automatically stub them.