What is program verification in c plus plus?

Answer 1

Program verification typically uses static analysis software to analyse program source code. Much of this is done by the compiler itself, however the compiler's primary job is to ensure the code will compile, not that it is logically correct, or efficient, or that it will actually solve the problem.

For instance, the following is perfectly acceptable as far as the compiler is concerned:

if (true) {

}

else if (true) {

// unreachable

}

else {

}

However, program verification will fail because the else if (true) clause is unreachable.

Similarly, it can happen that the then clause is exactly the same as the else clause:

int x;

if (true)

{

x = 42;

}

else

{

x = 42;

}

Problems such as these can be extremely subtle. The compiler will issue no warnings and the program will appear to work exactly as intended, but they are problems nonetheless. In these cases, program efficiency will be affected. They both produce programs that will be slightly larger than they need to be, but the second introduces an unnecessary decision along with duplicate code, thus affecting performance.

Throwing exceptions from a destructor is another problem.

struct foo

{

int m_data;

~foo() { if (!m_data) throw; }

};

In fact, it is illegal. Destructors must never throw exceptions. Yet the compiler allows it. If an exception could occur during destruction then it must be placed within a try...catch block and handled accordingly. Nothing should ever prevent an object from destroying itself.

PVS-Studio (see sources and related links below) is a good example of program verification software and is used primarily to validate open-source software. The website lists a number of problems that have been detected by the software, along with some examples of these problems.