The verification of real-life C/C++ code is inherently hard. Not only are there numerous challenging language constructs, but the precise semantics is often elusive or at best vague. This is even more true for systems software where non-ANSI compliant constructs are used, hardware is addressed directly and assembly code is embedded. In this work we present a lightweight solution to detect software bugs in C/C++ code. Our approach performs static checking on C/C++ code by means of model checking. While it cannot guarantee full functional correctness, it can be a valuable tool to increase the reliability and trustworthiness of real-life system code. This paper explains the general concepts of our approach, discusses its implementation in our C/C++ checking tool Goanna, and presents some performance results on large software packages.
展开▼
机译:真实生活中的验证C / C ++代码本质上很难。不仅有许多有挑战性的语言结构,而且精确的语义往往难以捉摸或以最佳含糊不清。对于使用非ANSI兼容构造的系统软件,这更为真实,直接解决硬件,并嵌入汇编代码。在这项工作中,我们提供了一种轻量级解决方案来检测C / C ++代码中的软件错误。我们的方法通过模型检查执行C / C ++代码的静态检查。虽然它无法保证全功能正确性,但它可以是提高现实生活系统代码的可靠性和可信度的有价值的工具。本文介绍了我们方法的一般概念,讨论了其在我们的C / C ++检查工具Goanna中的实现,并在大型软件包上展示了一些性能结果。
展开▼