Poszukuję narzędzia, które może statycznie wykrywać niezmienniki w programach C. Sprawdziłem Daikon, ale odkrywa niezmienniki tylko dynamicznie.Czy istnieje niezmienne narzędzie do wykrywania C dla programów statycznych?
Czy jest dostępne narzędzie do tego, czego szukam? Dzięki!
Jeśli masz na myśli słowo "niezmiennik" w najszerszym tego słowa znaczeniu, ponieważ strona z linkami do Daikon jest używana, to praca wielu narzędzi do analizy statycznej może być opisana jako "odkrywanie niezmienników", może po prostu nie są to ekspresyjne niezmienniki, których szukałeś dla.
Analiza wartości Frama-C gromadzi wyniki, możliwe wartości wszystkich zmiennych, dla każdej instrukcji. Pod koniec analizy może zatem prezentować nierelacyjne informacje na temat zmienności domeny każdej zmiennej w programie, przy każdym zestawieniu. W this screenshot niezmiennikiem jest to, że S jest zawsze 0, 1, 3 lub 6 tuż przed wybraną instrukcją, dla wszystkich wykonań tego deterministycznego programu.
Dwa ukryte parametry w pytaniu to kształt niezmienników, którymi jesteś zainteresowany, oraz kształt programów, dla których chcesz znaleźć te niezmienniki. Na przykład SLAM, o którym mowa w odpowiedzi Iry, został zaprojektowany do pracy nad kodem sterownika urządzenia i do wnioskowania o niezmiennikach, które zawierają jedynie informacje niezbędne do zweryfikowania właściwego wykorzystania systemowych funkcji API. Inne narzędzie, Astrée, słynie z bardzo dobrej pracy polegającej na wniosko- waniu odpowiednich niezmienników do zademonstrowania bezpieczeństwa działania oprogramowania do sterowania lotem.
Dwa stopnie swobody tworzą bardzo dużą przestrzeń projektową. Nie znajdziesz niczego, co działa dla wszystkich programów w języku C i zawiera wszystkie niezmienniki, które mogą Cię zainteresować, ale jeśli zawęzisz pytanie do konkretnych domen aplikacji i rodzajów niezmienników, będziesz miał większe szanse na znalezienie odpowiednich odpowiedzi.
Zobacz The SLAM project: debugging system software via static analysis. Twierdzi, że wnioskuje niezmiennie statycznie, za to, o co prosiłeś, w języku C. Autor, Tom Ball, jest szeroko znany z gwiezdnej pracy w analizie programów.
Witam, dziękuję za odpowiedź. Interesują mnie niezmienniki o prostej strukturze, takie jak interwały (pola). Myślę, że analiza wartości Frama-C jest lepsza, ponieważ zapewnia nawet konkretne wartości, a nie tylko interwały. –
@VijayaraghavanMurali Cóż, istnieją różnego rodzaju kompromisy dotyczące tego, jakie informacje należy zachować i jakie informacje wyrzucić, i na przykład, analiza wartości Frama-C zachowuje zestawy wartości do 8 elementów, a następnie przełącza się na interwały z informacjami zgodnymi. Dotyczy to liczb całkowitych. W przypadku 'float' i' double' używa tylko przedziału, aby odzwierciedlić fakt, że nie są one często używane do reprezentowania wartości dyskretnych o indywidualnym znaczeniu. A dla adresów ... szczegóły znajdują się na http://frama-c.com/download/frama-c-value-analysis.pdf –