|
|
Static Analysis of C Programs
Malík, Viktor ; Zuleger, Florian (oponent) ; Strejček, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis proposes several original contributions to the area of static analysis of software with focus on low-level systems code written in C. The contributions are split into two parts, each related to a different area of static analysis, namely formal verification of (low-level) C code and static analysis of semantic equivalence of different versions of the same software. The first part proposes new analyses suitable for verification engines that perform automatic invariant inference using an SMT solver. The proposed solution includes two abstract template domains that use logical formulae over bit-vectors to encode the shape of the program heap and the contents of the program arrays. The shape domain is based on computing a points-to relation between pointers and symbolic addresses of abstract memory objects. The array domain is based on splitting the arrays into several non-overlapping contiguous segments and computing a different invariant for each of them. Both domains can be combined with value domains in a straightforward manner, which particularly allows our approach to reason about shapes and contents of heap and array structures at the same time. The information obtained from the analyses can be used to prove memory safety and reachability properties, expressed by user assertions, of programs manipulating data structures. All of the proposed solutions have been implemented in the 2LS framework and compared against state-of-the-art tools that perform the best in the relevant categories of the well-known Software Verification Competition (SV-COMP). Results show that 2LS outperforms these tools on benchmarks requiring combined reasoning about unbounded data structures and their numerical contents. The second part of the thesis is motivated by existence of software projects that undergo regular refactorings and modifications and yet need to ensure semantic stability of some of their core parts. This part proposes a highly-scalable approach for automatically checking semantic equivalence of different versions of large, real-world C projects, with a particular focus on the Linux kernel. The proposed method uses a novel combination of pattern matching with light-weight static analysis and control-flow transformations. The method checks preservation of the semantics of functions forming the API of the project being analyzed as well as of the semantics of its global variables, which typically hold various control parameters. For the latter, a specialised slicing procedure is proposed to slice out code influenced by these variables and concentrate the further analysis on that code only. Although the method cannot prove equivalence on heavily refactored code, it can compare thousands of functions in the order of minutes while producing a low number of false non-equality verdicts as our experiments show. The method has been implemented over the LLVM infrastructure in a tool called DiffKemp. Our results show that DiffKemp, unlike other existing tools, gives practically useful results even on projects of the size of the Linux kernel.
|
|
|
Refaktoring objektově orientované aplikace
Solárik, Martin ; Burget, Radek (oponent) ; Kreslíková, Jitka (vedoucí práce)
Tento dokument je magisterskou diplomovou prácou na tému refaktoring objektovo orientovanej aplikácie. Jej cieľom je zoznámiť sa s problematikou refaktoringu, jeho základnými princípmi, výhodami, nevýhodami a základnými používanými vzormi a získané znalosti aplikovať na reálnu aplikáciu. Dokument je rozdelený do niekoľkých častí. V úvode sa venujem definovaniu pojmu refaktoring, v ďalšej jeho základným princípom, výhodám, nevýhodám ako aj dôvodom prečo refaktoring používať. Tretia časť je venovaná vzorom refaktoringu, tvorí akýsi katalóg jednotlivých refaktoringov. Ďalšia časť je venovaná platforme .NET a nástrojom na podporu refaktoringu v tejto platforme. Predposledná kapitola sa venuje predstavením aplikácie a následnej aplikácii refaktoringu. Posledná časť nazvaná záver, je venovaná zhodnoteniu dosiahnutých výsledkov.
|
|
|
Refaktoring při vývoji software
Dilík, Ján ; Bartík, Vladimír (oponent) ; Kreslíková, Jitka (vedoucí práce)
Táto práca sa zaoberá problematikou využitia refaktoringu, pri vývoji objektovo orientovaných aplikácií. Osvetluje problematiku refaktoringu a jeho vlastnosti ovplyvnujúce vývoj softwarového projektu. Pred samotným refaktoringom je potrebné pokryt refaktorovaný systém testami. Samotný refaktoring je možné aplikovat v procese vývoja pri oprave chýb, kontrole kódu ale aj ako celkový refaktoring systému. V tejto práci sú uvedené dopady refaktorovania produktu OKbase firmy OKsystem s.r.o. a ich zhodnotenie vzhladom k refaktorovaniu objektovo orientovaných aplikácií.
|
|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Refactoring the Frontend of the DNA Analyser web application
Skvortsov, Mikhail
Tato práce zkoumá refaktoring stávajícího kódu do modernějšího frameworku, přičemž hlavním cílem je přechod starého projektu z Vue 2 na Vue 3 s využitím Vuetify. Zdůrazňuje význam předběžných kroků a metodologických strategií v softwarovém inženýrství a zabývá se praktickými aspekty použití technologie Docker a integrací CI/CD pipeline. Práce metodicky popisuje postupný proces refaktoringu, začínající aktualizací knihoven, pokračující různými fázemi restrukturalizace kódu a konče testováním, aby se zajistila funkčnost a spolehlivost. Tento komplexní přístup nejen aktualizuje technologický stack, ale také vylepšuje celkovou strukturu projektu.
|
|
|
Refaktoring systému pro sledování kvality dat ve vrcholovém detektoru Belle II
Bártík, Jáchym ; Kvasnička, Peter (vedoucí práce) ; Červenkov, Daniel (oponent)
Tato bakalářská práce se zabývá refaktoringem části kódu pro sledování kvality dat z vrcholového detektoru Belle II. Druhou částí práce je implementace sledování pohybů half-shellů pixelového a stripového vrcholového detektoru Belle II v čase. Po shrnutí základních informací o experimentu Belle II, jeho vrcholovém detektoru a softwarovém systému basf2 popíšeme funkční chování modulů pro sledování kvality dat. Analyzujeme kód modulů TrackDQM a AlignDQM a opravíme chyby, které jsme v nich našli. V rámci refaktoringu rozdělíme výpočty do více jednodušších částí a výrazně zredukujeme duplicitní kód. Nakonec přidáme histogramy reziduálů z half-shellů, které po vyhodnocení na reálných datech fitujeme a zobrazíme v závislosti na čase. Přínosem této práce je lépe udržovatelný a snáze rozšiřitelný kód, stejně jako opravy mnoha chyb. Dalším výsledkem je objevení pravidelných pohybů half-shellů, jejichž po- chopení může vést ke zlepšení alignmentu detektoru. 1
|
|
|
Visual Studio Refactoring and Code Style Management Toolset
Linka, Marek ; Ježek, Pavel (vedoucí práce) ; Krijt, Filip (oponent)
Dodržování konzistentního stylu je nezbytné pro udržení spravovatelného zdrojového kódu. V době, kdy složitost softwarových řešení neustále roste, je tento požadavek důležitější než kdy dřív. Většina komerčně dostupných nástrojů pro zvýšení productivity psaní kódu se ale zaměřuje více na refaktoring a podporu dodatečných technologií než na dodržování konzistentního stylu psaní. Rozhodli jsme se proto napravit tuto situaci tím, že naimplementujeme sadu nástrojů pro Visual Studio rozšiřitelnou pomocí zásuvných modulů zaměřenou na hledání a nápravu porušení stylistických pravidel v jazyku C#. Dokončením našeho záměru jsme vytvořili nástroj, který se hladce integruje s Visual Studiem a poskytuje uživatelům efektivní a intuitivní prostředky pro zlepšení spravovatelnosti jejich kódu. Powered by TCPDF (www.tcpdf.org)
|
|
|
Refaktoring systému pro sledování kvality dat ve vrcholovém detektoru Belle II
Bártík, Jáchym ; Kvasnička, Peter (vedoucí práce) ; Červenkov, Daniel (oponent)
Tato bakalářská práce se zabývá refaktoringem části kódu pro sledování kvality dat z vrcholového detektoru Belle II. Druhou částí práce je implementace sledování pohybů half-shellů pixelového a stripového vrcholového detektoru Belle II v čase. Po shrnutí základních informací o experimentu Belle II, jeho vrcholovém detektoru a softwarovém systému basf2 popíšeme funkční chování modulů pro sledování kvality dat. Analyzujeme kód modulů TrackDQM a AlignDQM a opravíme chyby, které jsme v nich našli. V rámci refaktoringu rozdělíme výpočty do více jednodušších částí a výrazně zredukujeme duplicitní kód. Nakonec přidáme histogramy reziduálů z half-shellů, které po vyhodnocení na reálných datech fitujeme a zobrazíme v závislosti na čase. Přínosem této práce je lépe udržovatelný a snáze rozšiřitelný kód, stejně jako opravy mnoha chyb. Dalším výsledkem je objevení pravidelných pohybů half-shellů, jejichž po- chopení může vést ke zlepšení alignmentu detektoru. 1
|
|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Rozvoj IS pro studentskou organizaci
Dao, Ha My ; Palovská, Helena (vedoucí práce) ; Tomášková, Barbora (oponent)
Tato bakalářská práce se zabývá analýzou již existující databáze a jejím rozvojem pro budoucí použití. Databáze náleží informačnímu systému zvanému BuddyIS, který je využíván studentskou neziskovou organizací ESN VŠE Praha - Buddy System. Cílem práce je konsolidace stávající databázové struktury, čehož lze dosáhnout pomocí refaktoringu a návrhu nových prvků. Práce je zpracována na základě znalosti fungování organizace a jejího operačního systému, které autorka získala svým působením v organizaci. Aktuální požadavky jsou vydedukovány z konzultací se zainteresovanými osobami. Přínosem práce je položený základ pro další rozvoj celého informačního systému a dále vzniklá dokumentace, která poslouží další generaci členů ve spolku.
|
host ::
RSS.