静态分析和符号执行中的错误检测答案

【问题标题】：error detection in static analysis and symbolic execution静态分析和符号执行中的错误检测
【发布时间】：2016-07-23 09:09:34
【问题描述】：

静态分析（例如编译器）可以检测到哪些错误，而符号执行无法检测到？符号执行可以检测到静态分析无法检测到的哪些错误？比如符号执行可以检测语法错误吗？

【问题讨论】：

【解决方案1】：

简而言之，静态分析能够发现编码问题，例如不良做法。例如，如果您（不必要地）将类字段声明为公共，静态分析工具可能会警告您该字段应声明为私有。然而，“最干净”的代码不一定是没有错误的。尽管在某些代码中没有发现任何不当行为，但代表编码器的不正确推理可能会导致（稍后）运行时崩溃。

例如，如果我们开发干净的代码来实现一个计算器，那么静态分析工具不会输出任何警告，但是如果我们忘记验证输入以防止用户尝试除以零，那么我们的计算器最终会在运行时崩溃。

另一方面，符号（或Concolic）执行执行目标程序，因此它们有可能实现程序的任何可能的运行时执行状态，例如由错误引起的运行时错误。在上述计算器示例中，符号执行会发现运行时故障，并且还会告诉我们哪些输入会导致此类故障。要回答您的最后一个问题，符号执行并不是要检查代码的质量。

理想情况下，我们应该在发布软件之前同时使用两者。

【讨论】：

感谢您的回复。如果我用语法错误符号执行程序会发生什么？
如果程序有一个 synthax 错误它不会编译，那么你如何执行它（符号或其他）？
没错。解释型语言呢？
能否检测出类型不兼容等语义错误？还是只能检测逻辑错误？
没有。符号执行是一种执行形式，意味着它通过您在日常使用目标应用程序时可能遇到的任何执行路径来执行应用程序。问题是，其中一条路径可能会导致失败：在测试期间最好提前检测到它，而不是在日常使用期间检测到它。