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… ☹

Weitere Artikel

Dark Mode für Firefox und Thunderbird

Video Thumbnails unter Windows erstellen

Eindrücke aus Red Dead Redemption 2

Neuer Bluray Player: PS4

How to hardware reset the new Oura ring

Neuer Monitor: Dell S2716DG

Ein paar Bilder

Endlich da: Mein Oura Ring

Quick changelog with git

Pik Ass in Destiny 2