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.
The software verifies each constructor by creating an object using the constructor. If a constructor does not exist, the software uses the default constructor.
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 generatedmain
calls all public and protected methods instead of just the uncalled ones. For more information, seeFunctions to call within the specified classes (-class-analyzer-calls)
.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 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 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
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
, thestack::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:
Create an explicit instance of the class.
Define a
typedef
of the instance and provide thattypedef
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:
Add the following code to your Polyspace project.
template class calc<int>; typedef calc<int> my_template;
Provide
my_template
as argument of the option Class. SeeClass (-class-analyzer)
.
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:
You can analyze class
A
just by providing its code to the software. This corresponds to the previous “Simple Class” section in this chapter.You can analyze class
B
class by providing its code and the classA
declaration. In this case,A
code will be stubbed automatically by the software.You can analyze class
B
class by providingB
andA
codes (declaration and definition). This is a “first level of integration” verification. The class analyzer will not callA
methods. In this case, the objective is to find bugs only in the classB
code.You can analyze class
C
by providing theC
code, theB
class declaration and theA
class declaration. In this case,A
andB
codes will be stubbed automatically.You can analyze class
C
by providing theA
,B
andC
code for an integration verification. The class analyzer will call all theC
methods but not inherited methods fromB
and A. The objective is to find only defects in classC
.
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:
You can analyze classes
A
andB
separately just by providing their codes to the software. This corresponds to the previous “Simple Class” section in this chapter.You can analyze class
C
by providing its code withA
andB
declarations.A
andB
methods will be stubbed automatically.You can analyze class
C
by providingA
,B
andC
codes for an integration verification. The class analyzer will call all the C methods but not inherited methods fromA
and B. The objective is to find bugs only in classC
.
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.