Frama-C -

Frama-C

Deweloperzy	Commissariat à l'Énergie Atomique ( lista CEA ) i Inria
Magazyn	git .frama-c .com /pub /frama-c
Napisane w	OCaml
System operacyjny	Microsoft Windows , FreeBSD , OpenBSD , Linux , Mac OS X
Dostępne w	język angielski
Typ	Weryfikacja formalna , Statyczna analiza kodu
Licencja	głównie LGPL , niektóre części na licencjach BSD
Strona internetowa	frama-c .com

Frama-C oznacza ramy do modułowej analizy programów C. Frama- C to zestaw interoperacyjnych analizatorów programów dla programów C. Frama-C została opracowana przez francuski Commissariat à l'Énergie Atomique et aux Énergies Alternatives ( CEA-List ) i Inria . Otrzymał również dofinansowanie z Core Infrastructure Initiative . Frama-C jako analizator statyczny , sprawdza programy bez ich wykonywania. Wbrew nazwie oprogramowanie nie jest związane z francuskim projektem Framasoft .

Architektura

Frama-C ma modułową architekturę wtyczek porównywalną z architekturą Eclipse (oprogramowanie) lub GIMP .

Frama-C opiera się na CIL ( C Intermediate Language ) do generowania abstrakcyjnego drzewa składni . Drzewo składni abstrakcyjnej obsługuje adnotacje napisane w języku specyfikacji ANSI/ISO C (ACSL).

Kilka modułów może manipulować abstrakcyjnym drzewem składni , aby dodać adnotacje ANSI/ISO C Specification Language (ACSL). Wśród często używanych ^{[ niejasnych ]} wtyczek są:

Analiza wartości – oblicza wartość lub zestaw możliwych wartości dla każdej zmiennej w programie. Ta wtyczka wykorzystuje abstrakcyjne techniki interpretacji i wiele innych wtyczek korzysta z jej wyników.
Jessie – weryfikuje właściwości w sposób dedukcyjny. Jessie polega na zapleczu Why or Why3, aby umożliwić wysyłanie zobowiązań dowodowych do automatycznych programów dowodzących twierdzeń , takich jak Z3, Simplify, Alt-Ergo lub interaktywnych programów dowodzących twierdzeń, takich jak Coq lub Why. Za pomocą Jessie można udowodnić, że implementacja sortowania bąbelkowego lub zabawkowego systemu głosowania elektronicznego spełnia ich odpowiednie specyfikacje. Wykorzystuje model pamięci separacji inspirowany logiką separacji .
WP (Weakest Precondition) – podobnie jak Jessie , weryfikuje właściwości w sposób dedukcyjny. W przeciwieństwie do Jessie skupia się na parametryzacji w odniesieniu do modelu pamięci. WP jest przeznaczony do współpracy z innymi wtyczkami Frama-C, takimi jak wtyczka do analizy wartości, w przeciwieństwie do Jessie, która kompiluje program C bezpośrednio do języka Why. WP może opcjonalnie używać platformy Why3 do wywoływania wielu innych automatycznych i interaktywnych programów dowodowych.
Analiza wpływu – podkreśla wpływ modyfikacji w kodzie źródłowym C.
Slicing – umożliwia cięcie programu . Umożliwia generowanie mniejszego nowego programu C, który zachowuje niektóre podane właściwości.
Kod zapasowy – usuwa bezużyteczny kod z programu C.

Inne wtyczki to:

Dominatory – oblicza dominatory i postdominatory wypowiedzi.
Z analizy – oblicza zależności funkcjonalne.

Cechy

Frama-C może być używana do następujących celów:

Aby zrozumieć kod C, którego nie napisałeś. W szczególności Frama-C umożliwia obserwację zestawu wartości, podzielenie programu na krótsze programy i nawigację w programie.
Aby udowodnić własności formalne kodu. Używanie specyfikacji napisanych w języku specyfikacji ANSI/ISO C umożliwia zapewnienie właściwości kodu dla każdego możliwego zachowania. Frama-C obsługuje liczby zmiennoprzecinkowe.
Aby wymusić standardy kodowania lub konwencje kodu w kodzie źródłowym C za pomocą niestandardowych wtyczek
Instrumentować kod C pod kątem niektórych luk w zabezpieczeniach

Zobacz też

SPARK (język programowania)

Linki zewnętrzne

Kategorie: