Archive
Archive for June, 2010
Aliasing and how to control it
June 22, 2010
4 comments
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
June 7, 2010
2 comments
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;
}
Need help with using C or C++ in critical systems? Click on my picture above.
David Crocker's Verification Blog 