Archive

Archive for March, 2010

Verifying loops: proving termination

March 31, 2010 6 comments

If you’ve stuck with me so far in this mini-series on verifying loops, give yourself a pat on the back  before reading further. When it comes to formal verification of single-threaded software, loops are the most challenging constructs to verify. Read more…

Verifying loops – part 2

March 29, 2010 2 comments

Last time I showed how it was possible to analyse a loop-free and recursion-free program or function to determine its semantics (i.e. its weakest precondition and its postcondition), but that this didn’t work when we have loops. To make it possible to analyze loops thoroughly, Read more…

Verifying loops in C and C++ (intro)

March 22, 2010 1 comment

When it comes to formal verification of single-threaded programs, one of the hardest constructs to verify is the humble loop. If a function contains no loops and no function calls, then a static analyser can trace through the function, looking for constructs (such as indexing an array, or dividing one number by another) that have an implied precondition Read more…

Making sure variables are initialized

March 18, 2010 5 comments

One source of program bugs is use of variables before they have been initialized. In C/C++ all static variables get zero-initialized if they have no specified initialization, so it is only local variables we need to worry about. Bugs caused by use of uninitialized local variables can be particularly nasty, because the value of such a variable depends on whatever previously occupied the same stack location. Read more…

Using and Abusing Unions

March 12, 2010 4 comments

The C union type is one of those features that is generally frowned on by those who set programming standards for critical systems, yet is quite often used. MISRA C 2004 rule 18.4 bans them (“unions shall not be used”) on the grounds that there is a risk that the data may be misinterpreted. However, it goes on to say that deviations are acceptable for packing and unpacking of data, and for implementing variant records provided that the variants are differentiated by a common field. Read more…

Safer arrays: using a C++ array class

March 9, 2010 5 comments

In a previous post, I remarked that arrays in C leave much to be desired, and that in C++ it is better to avoid using naked arrays. You can avoid naked arrays in C++ programming by wrapping them up in a suitable array class instead. The Joint Strike Fighter C++ Coding Standards document takes a similar view; rule 97 in that standard states: Read more…

How (un)safe is pointer arithmetic?

March 3, 2010 10 comments

I recognize that this is a controversial topic – if you’re a safety-critical professional using C or C++, I’d be glad to hear your views.

Using explicit pointer arithmetic in critical software is generally frowned upon. MISRA 2004 rules 17.1 to 17.3 prohibit some particular cases of explicit pointer arithmetic that do not give rise to well-defined results. Read more…