3 ms·
One of the really nice outcomes of this approach is that it allows you to use different optimisation levels. Other approaches try to bypass the compiler by ver
by als0 8y ago
One of the really nice outcomes of this approach is that it allows you to use different optimisation levels.
Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation.
- monocasa 8y ago> Other approaches try to bypass the compiler by verifying the generated binary against the semantics of the source code (treating the compiler itself as a black box). The major drawback is that you had to completely disable all optimisation. sel4 verfies the binary against the specification, and lets you use optimization. Once you've extracted the flow graphs from the binary, following the optimizations isn't difficult.
- sanxiyn 8y agoYes, AutoCorres works, but it is somewhat user hostile, even for these tools, or compared to CompCert. CompCert looks and feels like a compiler, AutoCorres isn't. https://github.com/seL4/l4v/tree/master/tools/autocorres https://github.com/seL4/l4v/tree/master/tools/autocorres