C++ クラスの検証

クラスの検証

C++ などのオブジェクト指向言語は再利用目的で設計されています。そのような言語でコードを開発するとき、クラスが配置されるすべてのコンテキストを知っているとは限りません。考えられるどのコンテキストに対しても欠陥がない場合、クラスまたはクラスファミリの再利用は安全です。

考えられるすべてのコンテキストに対してクラスを安全にするには、ロバスト性検証を実施し、できるだけ多くのランタイムエラーを取り除きます。

Polyspace^® Code Prover™ は既定でロバスト性検証を実施します。ソフトウェアにクラスメソッドの定義とともにクラス定義を設定する場合、クラスのすべての使用をシミュレーションします。メソッド定義の一部が欠落していると、ソフトウェアは自動的にこれらをスタブします。

ソフトウェアはコンストラクターを使用してオブジェクトを作成し、各コンストラクターを検証します。コンストラクターが存在しない場合、ソフトウェアは既定のコンストラクターを使用します。
ソフトウェアは、以下の内容を前提として、これらのオブジェクトのパブリッククラス、静的クラス、保護されたクラスのメソッドを検証します。
- メソッドは任意の順序で呼び出される可能性がある。
- メソッドパラメーターはそのデータ型に許容される任意の値を取る可能性がある。
この検証を実施するために、コード内の他の場所で呼び出されていないメソッドを呼び出す main 関数が既定で生成されます。すべてのコンテキストに対してすべてのメソッドを検証する場合、この動作を修正します。それにより、生成された main は呼び出されていないメソッドだけを呼び出すのではなく、すべてのパブリックメソッドおよび保護されたメソッドを呼び出します。詳細は、指定クラス内で呼び出す関数 (-class-analyzer-calls) を参照してください。
ソフトウェアはこれらのオブジェクト (存在する場合) のデストラクターを呼び出し、検証します。

クラスを検証するとき、Polyspace は特定の仮定を行います。

コードの構成要素仮定

グローバル変数

コードの構成要素	仮定
グローバル変数	明示的に初期化されていない限り、各メソッドでは、グローバル変数はその型に許容される任意の値を取る可能性があります。たとえば、次のコードでは Polyspace は `globvar1` がその型に許容される任意の値を取る可能性があると仮定しています。したがって、オレンジの [ゼロ除算] が `globvar1` による除算に表示されます。ただし、`globvar2` は明示的に初期化されているため、`globvar2` による除算での [ゼロ除算] チェックはグリーンです。 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 は `m_loc.x` が初期化されていない可能性があると仮定しています。したがって、[未初期化変数] オレンジエラーが `getMember` メソッドの `x` で表示されます。チェックの後、Polyspace は変数がその型に許容される任意の値を取る可能性があると仮定します。したがって、オレンジの [オーバーフロー] が `show` メソッドの加算演算上に表示されます。 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; }; };

明示的に初期化されていない限り、各メソッドでは、グローバル変数はその型に許容される任意の値を取る可能性があります。

たとえば、次のコードでは Polyspace は globvar1 がその型に許容される任意の値を取る可能性があると仮定しています。したがって、オレンジの [ゼロ除算] が globvar1 による除算に表示されます。ただし、globvar2 は明示的に初期化されているため、globvar2 による除算での [ゼロ除算] チェックはグリーンです。

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 は m_loc.x が初期化されていない可能性があると仮定しています。したがって、[未初期化変数] オレンジエラーが getMember メソッドの x で表示されます。チェックの後、Polyspace は変数がその型に許容される任意の値を取る可能性があると仮定します。したがって、オレンジの [オーバーフロー] が show メソッドの加算演算上に表示されます。

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 }

クラスアナライザーはコンストラクターを呼び出してから、メソッドを任意の順序で何度も呼び出します。

このクラスの検証によって、以下の 2 つの問題が明らかになっています。

stack::push メソッドが配列の最後の要素の後に書き込みを行い、28 行目で OBAI オレンジチェックとなる場合がある。
push の前に呼び出されると、stack::top メソッドは要素 -1 にアクセスして、13 行目で OBAI および NIV チェックとなる。

これらの問題を解決すると、このクラスのランタイムエラーがなくなります。

テンプレートクラス

テンプレートクラスにより、クラスの操作が処理するデータ型の明示的な知識がなくてもクラスを作成できます。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-analyzer)を参照してください。

抽象クラス

実際には、抽象クラスのインスタンスを作成することはできません。そのため、解析することもできません。ただし、純粋な宣言を削除することで検証を容易に確立できます。これは、たとえば抽象クラスの定義を次のように変更することで実現できます。

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

抽象クラスが検証のために提供されると、ソフトウェアは自動的に変更を行い、抽象クラスの検証中に純粋なバーチャル関数 (上記の例では abstract_func) は無視されます。

これは、生成された main からの呼び出しは行われず、関数は完全に無視されることを意味します。さらに、関数が別のものに呼び出されると、純粋なバーチャル関数がスタブされ、呼び出しにはメッセージ "call of virtual function [f] may be pure" と共にオレンジチェックが付きます。

次のクラスを考えます。

A は抽象クラスです。

B は単純クラスです。

A および B は C の基底クラスです。

C は抽象クラスではありません。

クラス A のオブジェクトを作成できないため、他のクラスと分けてこのクラスを解析することはできません。したがって、クラス A を Polyspace クラスアナライザーに指定することはできません。もちろん、クラス C を前項「多重継承」と同じ方法で解析することは可能です。

静的クラス

クラスが静的メソッドを定義する場合、生成された main では従来のクラスのように呼び出されます。

継承したクラス

関数が派生クラスで定義されていない場合、父のクラスから継承されているため表示されていても、生成された main で呼び出されません。以下の例では、クラス 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;};
};

2 つのメソッド Location::getx および Location::gety は派生クラスでは表示されていますが、クラス Point の解析時に生成された main にはこれらのメソッドが含まれません。

派生メンバーは、父のコンストラクターで明示的に初期化されていない場合に volatile であると見なされます。上記の例では、2 つのメンバー Location::x および Location::y が volatile であると見なされます。上記の例を現在の状態で解析すると、メソッド 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 クラスの解析のために D クラスコードを提供する必要はありません。

多重継承

次のクラスを考えます。

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 は、前項「抽象クラス」で説明したのと同じ方法で解析することは可能です。

バーチャル継承はクラスアナライザーの使用方法には影響しません。

クラスの統合

A および B クラスから継承され、AA および BB クラスのオブジェクトメンバーをもつ C クラスを考えてみましょう。

クラスの統合検証は、検証するクラス C と A、B、AA および BB に対して提供するコードからなります。定義が欠落していると、ソフトウェアは自動的にスタブします。

参考

C++ コード検証用のコンテキストを設定する