Static analysis is a difficult task, partly because programming languages are extremely rich, and have intricate semantics with architecture-dependent aspects. We have therefore chosen to design Newspeak, a kernel language dedicated to the purpose of static analysis. And we have implemented a front-end, C2Newspeak, that translates C programs into Newspeak. Thus, any static analysis algorithm that uses this front-end, is preserved from the aforementioned sources of complexity. This paper fully presents the syntax and precise semantics of Newspeak. The design rationale of the language is explained and the advantages for static analysis highlighted. The various details of the translation from C to Newspeak are shown on examples. C2Newspeak was made to compile embedded C programs of a few million lines of code. It is, as well as a few other utilities, provided as free software under the LGPL.
Publié par EADS IW/SEBibTeX Document Publications autour de Newspeak