This master’s thesis addresses the challenge of enhancing the usability of sound static analyzers, specifically focusing on the state-of-the-art data race verifier Goblint. The aim is to soundly post-process the warnings generated by Goblint to make them more understandable for developers, thereby increasing the adoption of sound analyzers in practice. The thesis adapts and extends the warning repositioning algorithm of Muske et al. for data race warnings in multi-threaded C programs. Contributions include identifying and implementing a potential solution within the Goblint analyzer, extending the method for data races, and evaluating and analyzing the adapted algorithm in terms of the reduced distance between possible causes and warnings, as well as the impact on the quality of data race warnings.
Static analysis is a useful method for determining properties of programs without executing them. Goblint is a static analyser for the C programming language developed at the University of Tartu. During static analysis, Goblint determines many properties of the program, for example possible values of variables at different points in the program. These results are useful to understand the program being analysed, as well as the behavior of the Goblint analyses themselves. However, currently there is no good way to visualize them. Existing tools display the information in a raw and difficult to interpret form. In this thesis the initial version of one approach to visualize this information is implemented. The implemented approach is a special type of debugger, called an abstract debugger, which uses the same interface as a standard debugger, but instead of executing the program, it simulates program execution using the Goblint analysis results. The initial version of the abstract debugger is implemented and feedback for it is gathered from Goblint developers. The implemented abstract debugger is a step forward compared to existing tools for viewing Goblint analysis results.