### Archive

Archive for the ‘C and C++ in critical systems’ Category

## Verifying pointer arithmetic

Today I’ll look at whether code that uses pointer arithmetic is any harder to verify than equivalent code that does not use pointer arithmetic.

Consider this function for copying an array (or part of an array) into another array (or part of another array):

```void arrayCopy(const int* src, int* dst, size_t num) {
size_t i;
for (i = 0; i < num; ++i) {
dst[i] = src[i];
}
}```

## Run-time checks: Are they worth it?

One of the criticisms levelled against the use of C in safety-critical software is that the C language does not provide run-time checks automatically. For example, when indexing into an array, there is no check that the index is in bounds. Likewise, when doing integer arithmetic in C, there is no check for arithmetic overflow. Read more…

## Aliasing and how to control it

Today I’ll start by writing a simple function that determines the maximum and minimum of two integers. We want to return two values, and C doesn’t make that easy unless we declare a struct to hold them. So I’ll pass two pointers to where I want the results stored instead. Here goes:

```#include "arc.h"
void minMax(int a, int b, out int *min, out int *max)
post(*min <= a; *min <= b; *min == a || *min == b) post(*max >= a; *max >= b; *max == a || *max == b)
{ *min = a < b ? a : b;
*max = a > b ? a : b;
}```

I’ve highlighted the ArC annotations in green. Read more…

## Verifying absence of integer overflow

One class of errors we need to guard against when writing critical software is arithmetic overflow. Before I go into detail, I invite you to consider the following program and decide what it prints:

```#include <stdio.h>
int main(int argc, char *argv[]) {
unsigned int x = 42;
long y = -10;
printf("%s\n", (x > y ? "Hello, normal world!" : "Hello, strange world!"));
return 0;
}```

## Specification with Ghost Functions

In my previous post I showed that the C expression sublanguage extended with quantified expressions (forall and exists) is insufficient to allow some specifications to be expressed. I presented this function (annotated with an incomplete specification) to average an array of data:

```int16_t average(const int16_t * array readings, size_t numReadings)
{
int sum = 0;
size_t i;
for (i = 0; i < numReadings; ++i)
keep(sum == ? /* sum of first i elements of readings */ )
{
}
}```

## Expressing the Inexpressible

`forall ind in arr.indices :- arr[ind] >= 0 && arr[ind] <= 100`