Current State

Oproti mé diplomové práci (viz https://www.fit.vut.cz/study/thesis/24185) bylo navíc implementováno zejména následující:

• Wrappery nad zámky. Uvažují se 3 případy s nevyváženým zamykáním:

  1. Zámek je lokální proměnná - zámek se nepropaguje výše.
  2. Zámek je globální proměnná - zámek se propaguje výše s daným názvem zámku.
  3. Zámek je parametr funkce - zámek se propaguje výše s pozicí parametru zámku (volající dané funkce si tam pak dosadí název zámku podle použitého argumentu).

• Přidána spousta nových testů pro ověřování správného fungování analýzy, překladu, instalace atd. Všechno se to spouští automaticky přes GitHub Actions.

• Přidána možnost uvažovat v atomických množinách pouze metody ze stejné třídy (pro C++ a Java). Specifikovat, které třidy to budou, lze přes parametr analýzy. Budou se pak uvažovat pouze kontrakty, kde budou volání z těchto tříd.

• Dělá se ranking - počítá se, kolikrát se atomická množina vyskytuje. Pokud se vyskytuje jen jednou, tak se ignoruje. Tj. musí se vyskytovat alespoň dvakrát, aby se brala v potaz. Toto chování je možné zapínat/vypínat parametrem analýzy.

• Ignorují se volání nad lokálními (nesdílenými) objekty, protože takové volání asi nemají vliv na porušení atomicity. Pokud se pracuje s objekty (C++ a Java), tak se jako první parametr bere objekt, nad kterým se daná metoda volá (např. collection v collection.add(x)). Pokud jde o C, tak tam se bere první parametr volání funkce (např. collection v add(collection, x)). Toto chování se zapíná parametrem, protože je to celkem hrubá heuristika.