So many programs to verify, so little time

This post offers two C programs that look analyzable. Each is self-contained, not so small that verification is trivial, but not so big that it's a man-year effort. If it was me doing the work, I would see what Frama-C's value analysis can do, but if you decide to do it, it is your privilege to use any tool you like.

First example: extraitMax()

The first example comes, like another recent one, from Omar Chebaro's thesis. Like the previous example, I have no idea what it does:

int extraitMax(int Nd, int *Td){ 
	int G = 0; 
	int Nr = 0; 
	int Tr[100]; 
	int i = 1, fin = 0; 
	int tmp; 
	G = Td[1]; 
	Nr = Nd - 1; 
	for(i=0; i<Nd; i++){ 
		Tr[i] = Td[i]; 
	} 
	Tr[1] = Td[Nd]; 
	fin = 0; 
	while(i*2<=Nr && !fin){ 
		if( ((2*i)+1) <= Nr){ 
			if(Tr[i] < Tr[2*i] || Tr[i] < Tr[(2*i)+1]){ 
				if(Tr[2*i] >= Tr[(2*i)+1] ){ 
					tmp = Tr[i]; 
					Tr[i] = Tr[2*i]; 
					Tr[2*i] = tmp; 
					i = 2*i; 
				} 
				else{ 
					tmp = Tr[i]; 
					Tr[i] = Tr[(2*i)+1]; 
					Tr[(2*i)+1] = tmp; 
					i = (2*i)+1; 
				} 
			} 
			else 
				fin = 1; 
		} 
		else{ 
			if(Tr[i] < Tr[2*i]){ 
				tmp = Tr[i]; 
				Tr[i] = Tr[2*i]; 
				Tr[2*i] = tmp; 
				i = 2*i; 
			} 
			else 
				fin = 1; 
		} 
	} 
} 
int main(){ 
	int n = Frama_C_interval(2, 100); 
	int T[100]; 
	int i; 
	for(i = 0; i < n; i++){ 
		T[i] = Frama_C_interval(0, 127); 
	} 
	extraitMax(n, T); 
} 

Without having tried, there must be some alarms about the initializedness of arrays T and Tr that should easily go away by separately analyzing the different values of n.

It would be nice to show that this one terminates. This gives me an idea for one way the previously described option -obviously-terminates can be useful: it seems to me that if the analysis terminates when this option is set, it shows that all executions that are defined in the sense of the value analysis terminate. I am not saying that this method works for this program, though: it just looks like it might.

Second example: the 2006 IOCCC entry \stewart"

The actual winning entries to the pending contest are taking forever to appear but we'll always have the past entries. The program is here. You can get some additional files and information from the winners' page. IOCCC programs often use recursion libraries or syscalls but this one looks relatively analyzable. Just stub fopen() and each call to fscanf() appropriately.

This program uses floating-point.