Even though C is not considered a new language, it is used in several applications up to this day. Primarily, it is used in embedded systems, where performance matters. The low-level memory handling makes C convenient for this. Not only C is not dead language, but also it is expected to be used even more widely, due to the propagation of IoT (Internet of Things).
We have seen, C are mostly used in embedded systems. Embedded systems are not necessarily safety-critical systems, but in several cases, they can be found at safety-critical systems. Safety-critical systems are such systems, whose failures may have catastrophic consequences; human lives may be endangered, or severe financial, or environmental damage may arise. Think about the consequences, which occurs, when a controller gets out of order in an airplane, or in a nuclear reactor.
Software verification serves for avoiding such cases. It aims at finding the flaws in the software, or proving the absent of flaws. One of the most popular software verification method is testing. Though testing cannot prove mathematically the absent of flaws in a software, it still helps to make sure about the quality of the software. Since testing is a widespread procedure, there are lot of different methods for doing it. This thesis deals with code-based test generation.
In case of code-based test generation, we have access to the source code, automatic generation of the test cases is fully based on the source code. There are several methods to execute code-based test generation, for example symbolic execution, search-based algorithms, random algorithms, annotation-based test generation.
In this thesis a code-based test generation tools is being implemented and presented, which is capable of test generation, execution, and providing coverage results for programs, written in C language. For test input generation model checker is used, which is set to cover assert statements of the instrumented code. Since this kind of tools already exist, I try to pay attention to their incompleteness during the development of the tool.
After the tool is ready, I am going to examine it with both simple example C programs, and real world programs. Based on this, we can say, the tool is able to generate tests to basic C programs. It supports simple types, arrays, structures, but has limitations. The macros of C, structures inside structures, global variables are not handled. All in all, my tool does not reach the level of existing tools.