7

我希望这个问题不会超出 SO 的范围；如果是（在那种情况下很抱歉），请告诉我它属于哪里，我会尝试将它移到那里。

在 C/C++ 中用于静态代码分析的SAL 注释的概念对我来说似乎非常有用。以 MSDN 上错误实现的wmemcpy示例为例：Understanding SAL：

wchar_t * wmemcpy(
   _Out_writes_all_(count) wchar_t *dest,
   _In_reads_(count) const wchar_t *src,
   size_t count)
{
   size_t i;
   for (i = 0; i <= count; i++) { // BUG: off-by-one error
      dest[i] = src[i];
   }
   return dest;
}

MSDN 说“代码分析工具可以通过单独分析这个函数来捕获错误”，这看起来很棒，但问题是当我将此代码粘贴到 VS 2017 社区时，代码分析中不会弹出关于此的警告，即使使用启用所有分析警告。（其他类似的警告C26481 Don't use pointer arithmetic. Use span instead (bounds.1).。）

另一个应该产生警告的例子（至少根据对What is the purpose of SAL（Source Annotation Language）以及 SAL 1 和 2 有什么区别？ ）的回答，但没有：

_Success_(return) bool GetASmallInt(_Out_range_(0, 10) int& an_int);

//main:
int result;
const auto ret = GetASmallInt(result);
std::cout << result;

还有一个不正确警告的情况：

struct MyStruct { int *a; };

void RetrieveMyStruct(_Out_ MyStruct *result) {
    result->a = new int(42);
}

//main:
MyStruct s;
RetrieveMyStruct(&s);
 // C26486 Don't pass a pointer that may be invalid to a function. Parameter 1 's.a' in call to 'RetrieveMyStruct' may be invalid (lifetime.1).
 //  Don't pass a pointer that may be invalid to a function. The parameter in a call may be invalid (lifetime.1).

result显然标有_Out_and not_In_或_Inout_因此此警告在这种情况下没有意义。

我的问题是：为什么 Visual Studio 的基于 SAL 的代码分析看起来很糟糕；我错过了什么吗？Visual Studio Professional 或 Enterprise 在这方面可能更好吗？或者有没有可以更好地做到这一点的工具？

如果它真的很糟糕：这是一个已知问题吗？是否有计划改进这种类型的分析？

相关：Visual Studio 2013 静态代码分析 - 它有多可靠？

4

1 回答 1

1

函数契约，其中 SAL 注释是一种轻量级实现，可以在本地推理函数是否在做正确的事情，是否被错误地使用或相反。没有它们，您只能在整个程序的上下文中讨论错误的概念。正如文档所说，有了它们，就可以在本地说一个函数的行为是一个错误，并且您可以希望静态分析工具能够找到它。

即使有这个帮助，机械地验证一段代码没有错误仍然是一个难题。存在不同的技术，因为存在解决该问题的各种部分方法。它们都有优点和缺点，并且都包含大量启发式方法。循环是使预测程序的所有行为变得困难的部分原因，这些工具的实现者可能会选择不为极其简单的循环编写模式，因为这些模式在实践中很少使用。

如果它真的很糟糕：这是一个已知问题吗？是否有计划改进这种类型的分析？

是的，研究人员已经在这个主题上工作了几十年，并继续改进理论并将理论思想转化为实用工具。作为用户，您可以选择：

  • 如果你需要你的代码没有错误，例如因为它是为安全关键的上下文而设计的，那么你已经有了非常繁重的方法，基于在 V 循环的每个级别的密集测试，以及这种静态分析已经可以帮助您以更少（但一些）努力达到同样的信心水平。为此，您将需要比 SAL 注释更具表现力的合同规范。一个例子是C的ACSL 。
  • 如果您不愿意付出相当大的努力来确保代码没有错误并充满信心，您仍然可以利用这种静态分析，但在这种情况下，将发现的任何错误视为奖励。注释，因为它们具有正式定义的含义，即使在不涉及静态分析器的手动代码审查的上下文中，也可以用于分配责任。SAL 注释是专门为此用例设计的。
于 2018-08-22T08:05:40.897 回答