Splint liest C-Quellcode und findet typische Programmierfehler, das klappt ohne Änderung am Code. Mit etwas Zusatzaufwand ist aber noch mehr drin: In speziellen Kommentaren beschreibt der Entwickler sein Programm, damit ihn Splint besser versteht und noch mehr schmutzige Codestellen entdeckt.

Ohne Änderungen am Programmcode und ohne Flags beeindruckt der statische Semantikprüfer Splint[1] mit seinem detektivischen Spürsinn beim Finden von Fehlern. Ein Artikel in der letzten Ausgabe[2] beschrieb bereits, was Splint aus dem Stand beherrscht. Programmierer können das Tool aber noch wirksamer einsetzen, wenn sie ihr Programm mit speziellen Code-Kommentaren ergänzen. Die Kommentare erlauben es Splint, den Sourcecode besser zu verstehen. Der Prüfer ist dann in der Lage, noch eine ganze Reihe weiterer Probleme zu analysieren. Dazu gehören unter anderem:

• Unendlichen Schleifen
• Fehler bei der Speicherfreigabe (Memory Leaks)
• Dereferenzieren von Null-Zeigern
• Verstöße gegen Namenskonventionen
• Nicht passende Schnittstellen
• Buffer Overflows
• Unerreichbarer Code

Vor einfachen Problemen warnt bereits der C-Compiler. Je komplexer die Fallen sind, in die der Programmierer tappt, desto mehr Aufwand müssen Tools treiben, um die Fehler zu entdecken. Abbildung 1 stellt Ertrag und Nutzen dieser Werkzeuge gegenüber: Werkzeuge zur formalen Verifikation finden zwar die meisten Fehler, dazu ist jedoch ein beträchtlicher Aufwand nötig. Mit Splint bleibt der Aufwand gering, das Tool findet dennoch sehr viele Bugs.

Kommandos

Das Splint-Kommando kennt eine Reihe von Optionen und Parametern. Die Syntax lautet:

splint Flags -f Dateiname Programm

Dabei ist » Flags« eine Liste von Schaltern, die mehrere Arten der Überprüfung aktivieren oder deaktivieren.

Anders als bei den meisten Unix-Programmen deaktiviert ein Minuszeichen »-« die jeweilige Option, ein Pluszeichen »+« aktiviert sie. Zusätzlich gibt es Abkürzungen sowie Prüfstufen, die eine ganze Reihe von Flags gleichzeitig betreffen. Splint unterscheidet vier Stufen, auf denen es immer strengere Prüfkriterien anwendet: »-weak«, »-standard« (Default), »-checks« und »-strict« (siehe Kasten “Splint-Prüfstufen”).

Falls die Datei »~/.splintrc« existiert und lesbar ist, übernimmt Splint die Standardeinstellungen der Flags aus diesem File. Mit »-f Dateiname« kann man auch eine andere Datei verwenden. Folgender Aufruf überprüft das Programm »Beispiel1.c« aus Listing 1:

splint -checks +boundswrite 
  -exportheader Beispiel1.c

Mit diesen Parametern benutzt Splint die Prüfstufe »checks«, und zwar ohne die Prüfung »exportheader«, aber mit aktiviertem »boundswrite«.

Kluge Kommentare

Splint bezieht sein Wissen über den Sinn einzelner Codestellen nur aus dem vorliegenden Quellcode. Bei auffälligen Details kann Splint daher nicht wissen, was der Programmierer damit beabsichtigt oder ob es schlicht ein Fehler ist. Dies Hintergrundwissen kann der Programmautor in spezielle Kommentare packen und damit an Splint weitergeben.

Listing 1 enthält solche Kommentare: Die Main-Funktion in Zeile 3 nimmt eine Liste von Argumenten entgegen, die sie aber nie benutzt. Der Code-Kommentar »/*@unused@*/« verhindert, dass Splint eine Fehlermeldung ausgibt: Dem Programmautor ist bewusst, dass er die Variablen nicht verwendet, er setzt sie aber absichtlich ein. Solche Code-Kommentare beginnen immer mit »/*@« und enden mit »@*/«. Folgendes Kommando gibt eine Liste der möglichen Kommentare aus:

splint -help annotations

Ein verbreitetes Problem beim Entwickeln von Software sind ungültige Zeiger. Sie verursachen die Hälfte aller Fehler. Auch bei Bugs dieser Art hilft Splint. In Listing 1 hat sich ein kleiner, aber sehr unangenehmer Fehler eingeschlichen: Zeile 9 gibt Speicher frei, der einen String enthält. Zeile 10 versucht, genau diesen String auszugeben.

Im vorliegenden Beispiel ist das unkritisch und leicht zu bemerken, in realen Programmen können zwischen dem Freigeben des Speicherbereichs und dem verbotenen Zugriff aber Hunderte von Programmzeilen liegen. Während diese bearbeitet werden, könnte der Speicher beliebige andere Daten erhalten haben oder außerhalb des gültigen Adressbereichs liegen. Splint reagiert mit der folgenden Warnung:

Beispiel1.c:10:26: Variable dpointer 
used after being released

Schwieriger wird die Sache, wenn Speicheranforderung und -freigabe nicht im Hauptprogramm, sondern in Funktionen erfolgen. Das Programm in Listing 2 fordert in der Routine »allocmem()« Speicher an. Es erwartet in »get_data()« vom Benutzer eine String-Eingabe und kehrt diesen Text in »reverse_data()« um. Dann gibt es den String aus und den Speicher in »deallocmem()« wieder frei. In der vorliegenden Form führt das Programm unter anderem zu folgender Splint-Fehlermeldung:

linttest.c:70:8: Implicitly temp storage 
char_p passed as only param: free (char_p)

Splint meint, dass angeforderter Speicher nicht freigegeben wurde. Die Fehlermeldung verschwindet, wenn man den Code-Kommentar »/*@only@*/« direkt vor »char*« in Zeile 11 einfügt. Der Semantikprüfer weiß jetzt, dass es sich um eine exklusive Referenz handelt. Das bedeutet: Dieser Zeiger ist verpflichtet, den Speicherplatz, auf den er zeigt, wieder freizugeben. Die Verpflichtung kann er auf drei Arten an andere Zeiger übertragen:

• Der Zeiger wird als Parameter an eine Funktion übergeben.
  Dabei kommt das »only«-Attribut zum Einsatz.
• Er wird an eine externe Referenz über-geben, die das
  »only«-Attribut trägt.
• Er wird als Funktionsresultat übergeben, das auch mit dem
  »only«-Attribut versehen ist.

Nachdem er seine Verpflichtung auf einen anderen Zeiger übertragen hat, gilt der ursprüngliche Pointer als toter Zeiger, der nicht mehr verwendet werden darf. Dadurch kann Splint gewährleisten, dass das Programm einmal angeforderten Speicher wieder freigibt, und zwar genau ein Mal. Damit das alles richtig funktioniert, muss die Verpflichtung zur Speicherfreigabe einmal entstehen. Das passiert in den Routinen, die Speicher reservieren, etwa »malloc()« oder »calloc()«.

Splint bringt eigene Versionen der Header für Standardbibliotheken mit. Diese enthalten bereits Code-Kommentare, die Splint beim Überprüfen eines Programms automatisch verwendet. Die »malloc()«-Funktion sieht dort so aus:

/*@only@*/ /*@null@*/ 
void *malloc(size_t size);

Der Rückgabewert ist ein Zeiger, der auf einen Speicherbereich zeigt, den der Aufrufer wieder freigeben muss (»only«). Der Zeiger kann eventuell null sein. Durch einen Blick in die mit Splint gelieferten Header »standard.h« und »posix .h« kann man eine Menge über die Code-Kommentare lernen.

01 #include <stdlib.h>
02 
03 int main(/*@unused@*/ int argc, /*@unused@*/ char **argv)
04 {
05    char* dpointer=NULL;
06    dpointer = (char*)calloc((size_t)20, (size_t)1);
07    if (dpointer==NULL) return 1;
08    strcpy (dpointer, "Hello World");
09    free (dpointer);
10    printf("Ausgabe: %sn", dpointer); /* dpointer zeigt  ins Nirwana */
11    return 0;
12 }

Bibliotheken mit Code-Kommentaren

Das Gegenstück zu »malloc()« – die Funktion »free()« – sieht folgendermaßen aus:

void free(/*@only@*/ /*@out@*/ 
 /*@null@*/ void* ptr);

Diese Funktion nimmt als Parameter einen Zeiger auf einen Speicherbereich entgegen, den sie wieder freigeben muss (»only«, sie übernimmt also die Verantwortung). Die aufrufende Funktion darf den Bereich danach nicht mehr benutzen, sie hat die Verantwortung dafür abgegeben. Der Zeiger kann eventuell null sein, es kann daher vorkommen, dass der Speicherplatz nicht initialisiert ist (»out«).

Es ist auch möglich, die »only«-Zeiger anderen Pointern zuzuweisen. Diese müssen dann das Kommentar-Attribut »/*@temp@*/« tragen. Solche Temp-Zeiger dürfen weder Speicherplatz anfordern noch freigeben, auch darf das Programm nicht mehr auf sie zugreifen, nachdem es den Speicherplatz freigegeben hat. Damit alles auch bei unkommentierten Programmen gut funktioniert, sieht Splint alle Zeiger per Default als Temp an.

01 // Beispielprogramm 2
02 
03 #include <stdlib.h>
04 #include <stdio.h>
05 #define BUFSIZE 200
06 // Namenskonvention: Alle eigenen Typen beginnen
07 // mit "T_" und enthalten dann nur Kleinbuchstaben
08 /*@ +matchanyintegral +typeprefix T_&* @*/
09 
10 static /*@null@*/ char* allocmem(void) /*@modifies nothing@*/ ;
11 static void deallocmem(char*) ;
12 static int get_data (char *outputdata) /*@modifies outputdata@*/;
13 static int reverse_data(char *inputdata) /*@modifies inputdata@*/;
14 static int S_num;
15 
16 int main(/*@unused@*/ int argc, /*@unused@*/char **argv)
17 {
18    char* dpointer=NULL;
19    int char_cnt=0;
20    int space_cnt=0;
21    S_num=0;
22    dpointer = allocmem();
23 // if (dpointer==NULL) return 0;
24    char_cnt = get_data (dpointer);
25    char_cnt = reverse_data (dpointer);
26    printf ("Anzahl der Zeichen: %i Ausgabe: %sn", char_cnt, dpointer);
27    deallocmem (dpointer);
28    if (char_cnt ==0)
29    {
30       return 0;
31    }
32    else
33    {
34       return 0;
35    }
36    return 0; // Code ist unerreichbar
37 }
38 
39 int reverse_data(char *inputdata)
40 {
41    int i =0;
42    char c;
43    int a = strlen(inputdata);
44    while (i<=a/2-1)
45    {
46       c=*(inputdata+i);
47       *(inputdata+i) = *(inputdata+a-i-1);
48       *(inputdata+a-i-1)=c;
49 //    i++;
50    }
51    return a;
52 }
53 
54 int get_data (char *inputdata)
55 {
56    int i=0;
57    printf ("Eingabe eines Strings: ");
58    (void) fgets (inputdata, BUFSIZE-1, stdin);
59    S_num = strlen (inputdata);
60    return i;
61 }
62 
63 char* allocmem(void)
64 {
65    return (char*)malloc((size_t)BUFSIZE);
66 }
67 
68 void deallocmem(char* char_p)
69 {
70    free (char_p);
71    return;
72 }

Null-Zeiger

Ein verbreitete Falle bei C-Programmen sind Zugriffe auf Zeiger, die null sind. Wenn nichts anderes angegeben ist, nimmt Splint an, dass ein Zeiger nie null sein darf. Um das dennoch zu erlauben, muss es der Programmierer durch das Attribut »/*@null@*/« angeben. Die »malloc()«-Funktion ist wieder ein gutes Beispiel: Wenn kein Speicher verfügbar ist, gibt sie einen Null-Pointer zurück. Falls ein Programm diesen Zeiger jedoch dereferenziert, gibt Splint eine Fehlermeldung aus. Für Listing 2 lautet sie:

linttest.c:24:23: Possibly null storage 
dpointer passed as non-null param: 
get_data (dpointer)

Fügt man die auskommentierte Zeile 23 wieder ein, schweigt Splint. Es erkennt, dass die If-Abfrage verhindert, dass das Programm danach einen Null-Zeiger dereferenziert.

Korrekte Schnittstellen

Funktionen tauschen mit ihrer Aufrufumgebung Informationen durch ihre Schnittstelle aus. Funktionsprototypen beschreiben Typ und Anzahl dieser Schnittstellen. Es ist gute Programmierpraxis, genau zu dokumentieren, welche Funktionsargumente von einer Funktion geändert werden und welche sie unverändert lässt. Durch den Code-Kommentar »/*@modifies@*/« kann man Splint mitteilen, welche Funktionsargumente und welche globalen Variablen die Routine verändern könnte. Treten hier Widersprüche auf, deutet das auf einen Programmierfehler hin.

Diese Schnittstellenvereinbarungen bilden auch benutzerdefinierte Konstanten nach, vergleichbar zu »const« in C++. Splint prüft, ob ein Ausführungspfad Argumente ändert, die nicht in Modifies angegeben sind. Dazu muss die Option »+mods« gesetzt sein. Ein Fehler kann es aber auch sein, wenn die Funktion als Modifies angegebene Argumente nicht verändert. Um diese Überprüfungen zu aktivieren, muss das Flag »+mustmod« gesetzt sein. Diese Tests sind in der Prüfstufe »checks« enthalten.

Alle Routinen des Beispielprogramms sind mit dem Modifies-Code-Kommentar ausgestattet. Da die »get_data()«-Funktion die globale Variable »S_num« verändert, ohne dass dies im Modifies-Kommentar angegeben wurde, gibt Splint folgende Fehlermeldung aus:

linttest.c:58:2: Undocumented 
  modification of S_num: 
  S_num = strlen(outputdata)

Abbildung 1: Die meisten C-Compiler warnen nur vor einfachen Bugs. Komplexere Fehlerklassen benötigen entsprechend mehr Aufwand – bei Splint wählt der Programmierer die passende Prüfstufe (Grafik nach [3]).

Unendliche Schleifen

Splint kann auch herausfinden, ob eine Schleife unter Umständen nie endet. Das funktioniert allerdings nur in sehr einfachen Fällen, etwa in der Funktion »reverse_data()« des Beispielprogramms (Listing 2). Splint bringt folgende Fehlermeldung:

linttest.c:43:9: Suspected infinite loop.
  No value used in loop test (i, a) is 
  modified by test or loop body.

Leider verschwindet diese Fehlermeldung sofort, wenn man vor dem Ende der While-Schleife ein »i=3;« einfügt. Die Schleife ist immer noch unendlich, denn der Schleifenvariablen wird nur eine Konstante zugewiesen. Splint erkennt das Problem aber nicht mehr. Besser wäre »i++;«.

Splint prüft auch die Erreichbarkeit von Code. Das Return-Statement am Ende von »main()« kommt nie zur Ausführung, da bereits in der If-Abfrage zuvor beide Zweige eine Return-Anweisung enthalten. Folglich meldet Splint einen Bug. Falls diese Fehlermeldung nicht gewünscht ist, kann man sie lokal mit Hilfe eines Code-Kommentars abschalten: einfach vor dem Return diese Zeile einfügen

/*@ -unreachable @*/

und danach die Überprüfung wieder einschalten mit:

/*@ +unreachable @*/

Mit dieser Variante lassen sich spezielle Prüfungen gezielt an kritischen Stellen einschalten oder überflüssige und falsche Fehlermeldungen abstellen. Ein weiteres Beispiel dafür ist Zeile 8 in Listing 2: Das Flag »matchanyintegral« verhindert, dass Splint die Zuweisung von »size_t« an »int« für einen Fehler hält.

Kontrollierte Namenskonventionen

Um Code für alle, die damit arbeiten müssen, gut lesbar zu halten, sind Namenskonventionen sehr praktisch. Welche Konventionen ein Projekt nutzt, ist nicht so entscheidend – wichtig ist aber, dass alle Entwickler die Konventionen konsequent einhalten. Splint kann auch das überprüfen.

Einige Flags legen fest, wie die Namen von verschiedenen Arten von Variablen oder selbst definierten Typen auszusehen haben. Diese Flags beginnen mit dem Namen der Kategorie (etwa »local« für lokale Variablen) und dem Schlüsselwort »prefix«. Nach einem Leerzeichen folgt das Muster (Pattern) für diesen Namen. Es gibt mit Sonderzeichen die Regeln vor, denen die Namen unterliegen. Leider kann man keine regulären Ausdrücke anwenden. Zum Beispiel legt

/*@localprefix L_&* @*/

fest, dass alle lokalen Variablen mit »L_« anzufangen haben und danach nur kleine Buchstaben folgen dürfen (»*« bedeutet, dass das vorherige Zeichen beliebig oft hintereinander gilt).

Tabelle 1 zeigt die Kategorien und die Sonderzeichen für diese Regeln. Das Listing 2 enthält in der Zeile 8 ein weiteres Beispiel: Alle selbst definierten Typen müssen mit »T_« beginnen, gefolgt von Kleinbuchstaben.

Makros

Der Makro-Präprozessor ist ein mächtiges Werkzeug, er birgt aber viele Gefahren. Makros funktionieren als reine Textersetzung und durchbrechen damit die Syntax von C. Klassisches Beispiel ist ein Makro, das das Quadrat berechnet:

#define Quadrat(x) x*x

Diese Definition geht gut, wenn das Makro nur einzelne Werte erhält, etwa »Quadrat(i)«. Probleme treten auf, wenn man es als »Quadrat(i+1)« einsetzt. Der Präprozessor verwandelt diesen Text in »i+1*i+1«, das entspricht »i+i+1« und nicht »(i+1)*(i+1)«. Auch »Quadrat(i++)« ist problematisch, da die Langform »i++*i++« zu Implementations- spezifischem Verhalten führt. Mit dem Flag »+allmacros« aufgerufen überprüft Splint unter anderem Folgendes:

• Ein Makroparameter darf niemals in Verbindung mit dem
  Dekrement- oder Inkrement-Operator verwendet werden.
• Makroparameter müssen in Klammern eingeschlossen
  sein.
• Jeder Makroparameter ist nur genau ein Mal verwendbar.

Speicherüberlauf

Die Speicherüberläufe (Buffer Overflows) sind besonders gefährliche Fehler in C-Programmen. Viele Angriffe nutzen solche Bugs, Speicherzugriffe außerhalb der vorgesehenen Bereiche führen also zu ernsthaften Problemen. Splint verwaltet Speicherblöcke mit Hilfe der beiden internen Variablen »maxSet« und »maxRead«, die es automatisch für jeden Vektor anlegt.

Dabei bestimmt »maxSet« die Obergrenze, bis zu der das Programm den Speicherbereich beschreiben darf; »maxRead« ist die Obergrenze für Lesezugriffe. In einfachen Fällen genügt:

int myarray[10];
int i = 8;
myarray[i+4]=0;
myarray[i-12]=0;

Ist die Bounds-Checking-Option aktiviert, entdeckt Splint, dass der erste Zugriff auf das Array vermutlich über dessen Ende hinaus schreibt:

Possible out-of-bounds store: 
  myarray[i + 4]

Die negative Indizierung in der letzten Zeile erkennt das Tool leider nicht: Der Zugriff erfolgt auf Element 8-12, also -4, und damit vor dem Array-Beginn.

Wertebereiche fordern und garantieren

Die konkreten Werte der Indizes zur Laufzeit sind beim statischen Prüfen häufig nicht bekannt. Es gibt deshalb die Code-Kommentare »/*@ensure@*/« und »/*@require@*/«, um die Maximalwerte von Parametern festzulegen, die an Funktionsschnittstellen übergeben werden. Das erfordert aber einen sehr hohen Aufwand beim Programmierer und garantiert keinen Erfolg.

Als Konsequenz ist die Überprüfung von Buffer Overflows in keiner Prüfstufe enthalten, man muss sie immer separat mit den Flags »+boundswrite« und »+boundsread« aktivieren. Die Splint-Autoren stellen in[5] ihre Technik vor, mit der sie mögliche Buffer Overflows mit einem statischen Prüfprogramm entdecken, ohne das geprüfte Programm tatsächlich auszuführen.

In C ist es legal, einer Variablen eines Aufzählungstyps (»enum«) beliebige Integer-Werte zuzuweisen und nicht nur die in der Deklaration angegebenen Werte:

enum Wochentag =
  {Mo, Di, Mi, Do Fr, Sa, So};
Wochentag = 15;

Splint meldet hier einen Fehler, wenn es mit »-checks« aufgerufen wurde. Ebenso erkennt es, ob Variablen noch vor ihrer Definition benutzt werden und ob das geprüfte Programm die Rückgabewerte von Funktionen ignoriert.

Fazit

Tiefer gehende Informationen zu den Fähigkeiten von Splint sind im ausführlichen Benutzerhandbuch[3] zu finden. Den größten Nutzen verspricht Splint, wenn man es von Anfang an in den Entwicklungsprozess integriert und konsequent nutzt. Es dauert nicht länger, Programme mit Code-Kommentaren zu schreiben als ohne. Das gezielte Kommentieren zwingt aber dazu, beim Programmieren über die Bedeutung einer Variablen oder eines Parameters genauer nachzudenken, um gegebenenfalls entsprechende Code-Kommentare einzusetzen. Das kommt der Qualität der Programme zugute.

Splint ist eine große Hilfe beim Vermeiden von Fehlern, außerdem spart es viel Aufwand beim Debuggen. Die größte Schwäche von Splint ist sicherlich, dass es C++ nicht unterstützt. Allerdings steht das Tool unter der GPL und Projektleiter David Evans hat seine Hilfe angeboten, wenn sich jemand bereit erklärt, ein C++-Frontend zu schreiben. Das ist mit Sicherheit eine lohnende Aufgabe mit großem Nutzen für die Entwicklergemeinde. (fjl)