Static code analysis based on the syntactic and semantic model of source codes

OData support
Dr. Suba Gergely
Department of Control Engineering and Information Technology

The correct operation of the software is crucial. Flaws in safety-critical software systems can be disastrous, since they may cause not only significant damage to property but also a loss of life. Therefore, safety-critical software systems have to meet certain standards, complying them may contribute to error prevention.

The C language is one of the most common languages in developing safety-critical and especially embedded systems, since it is a well-tried language that is sufficiently close to low-level languages, and it has a lot of compilers and developing tools. One of the drawbacks of the language is that it is highly tolerant thus it is easy to make run-time mistakes.

A huge amount of bugs is only discovered during testing in runtime thus finding bugs and correcting them costs a lot of time and money. A static code analyser software can detect the errors during the compilation thus the developer can fix the bugs even during development.

During the design phase of my code analyzer, I got to know different popular programs, models and standards that support code analysis.

In my paper, I defined a subset of expressions of the C language without limiting the expressiveness of the language but reducing the possibilities for bugs in programs. The subset of the C is strongly-typed, grants the opportunity to narrow down the codomain of a type and restrict the set of the usable operations. These may provide a solution to manage the physical dimensions properly.

The C code is transformed into a model made by the EMF (Eclipse Modeling Framework), thus it is simple to handle. I defined Viatra queries and validation constraints to this model, which are based on graph pattern matching. When the user violates a constraint, the code analyser program reports it by an Eclipse IDE (Integrated Development Environment) plug-in that I developed based on the Eclipse CDT (C / C++ Development Tooling) plug-in. I defined test cases to detect and fix bugs made during the implementation.


Please sign in to download the files of this thesis.