Extending Safe C Support In Leon

As hardware designs get more robust and efficient, software can solve a wider range of challenges, each one more advanced than the previous one. The direct consequence is that software complexity grows continuously. Despite being used more frequently in development processes, traditional testing frameworks are not enough to avoid flaws in programs. Moreover, many company concerned by the security of their applications, especially in mission critical industries, spend a considerable effort and amount of money to write robust software certified by solid guidelines and standards. For embedded systems, MISRA C is a certification process commonly used which provides directives to write portable and maintainable C code while avoiding many pitfalls of the language. Leon takes an orthogonal approach by providing tools for formal verification of programs written in a subset of Scala. In a previous work we introduced GenC, a module for Leon that converts Scala applications into equivalent and safe C99 programs, allowing developers to leverage high-level feature of Scala to implement robust applications, even for embedded systems. The aim of this project is to augment Leon and GenC in order to support a larger fragment of Scala that includes inheritance, generic programming, additional numeric types, pattern matching and more. Additionally, we closely analyse the MISRA Guidelines and shape the generated C code to work towards compliance with its rules while taking advantage of the verification capabilities of Leon to automatically detect a variety of bugs. We discuss these improvements and new features by implementing the famous LZW compression/decompression algorithm as well as a kernel-based image processing algorithm and show that the produced native C programs are significantly more efficient both in terms of memory usage but also in terms of execution speed.