Sourcecode-Analyse mit Frama-C

Seit einigen Tagen interessiere ich mich für die Analyse von Sourcecode mittels Frama-C. Das ganze ist aus der Projektarbeit geboren, bei der ich mit Mathworks Polyspace zu tun habe und mich mit den Meldungen aus der Analyse herumschlagen darf. Leider wieder viel zu spät im inkrementell-iterativen Entwicklungszyklus und daher mit sehr viel Aufwand verbunden. Allerdings scheint es auch keine kostengünstige Alternative zu Polyspace zu geben.

Bis ich schliesslich über Frama-C stolperte. Damit kann der Quelltext analysiert werden, um Hinweise auf mögliche Probleme zu bekommen. Es gibt z.B. die Value Analysis mit deren Hilfe mögliche Werte und Wertebereiche für Variable bestimmt werden. Ich habe das ganze auf das folgende kleine Programm losgelassen:

MISSING CODE

Auf dieses kleine Programm habe ich dann Frama-C mit dem folgenden Aufruf losgelassen:

frama-c -val hello.c

Damit wird Frama-C angewiesen, das Value Analysis Plugin auf die Datei hello.c anzuwenden. Heraus kommt die folgende Ausgabe:

MISSING CODE

Sehr interessantes Ergebnis. Damit wird eine Prüfung der berechneten Werte möglich. Es wird quasi eine Äquivalenzklassenbildung automatisiert und mögliche Wertebereiche zurückgegeben. Frama-C kann noch sehr viel mehr, aber ich befinde mich gerade erst am Anfang der Reise. Ich denke, ich werde mich mit dem Tool noch weiter beschäftigen und prüfen, wie man das ganze in die bestehenden Prozesse integrieren kann. Und an welcher Stelle und für welche Projekte das überhaupt Sinn macht.

PS: Falls mir jemand sagen kann, wie man sinnvoll Quelltexte in Blogger einpacken kann, wäre ich sehr dankbar. Anscheinend zerschiessen pre-Tags das ganze Layout und werden von Blogger auch nicht wirklich gut abgespeichert. Nach jedem Speichern verschwinden Zeilen, werden Umbrüche zerstört… ☹