In the functional safety standard for the aviation industry, there is a requirement that the compiler does not generate "additional code". Additional code is defined as code that is found in the target assembly code, but not in the source code. In the general case, this is a hard problem, especially in the presence of compiler optimizations. In practice, therefore, this check is done on non-optimized code.
Manual verification requires that a sufficiently knowledgeable engineer compares every line of source code with its generated code. Needless to say, manual verification is very labor intensive and error prone.
Automatic verification tools compare the control flow graph of the source code and the target code, to verify that no new control flow edges are added. This method does not look at the code between control flow edges and is therefore also limited. We propose to improve on this method by a generic tool that compares the parse tree of the program to the generated assembly. By means of an interactive tool, a developer can teach the tool how patterns in the source code are matched to the target assembly. Any assembly that is constructed with known patterns can be automatically verified, leaving only a (hopefully) small number of cases to be verified manually. The task of this project is to build such a pattern recognition based tool.
- A pleasant working environment in Amsterdam
- Guidance when you need it
- An internship compensation