使用 SAL 注释的 Visual Studio Community 代码分析质量

Question

我希望这个问题不会超出 SO 的范围；如果是（对不起），请告诉我它属于哪里，我会试着把它移到那里。

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

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).。）

另一个应该产生警告的例子（至少根据an answer to What is the purpose of SAL (Source Annotation Language) and what is the difference between SAL 1 and 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_ 而不是_In_ 或_Inout_，因此在这种情况下此警告没有意义。

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

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

相关：visual studio 2013 static code analysis - how reliable is it?

Answer 1

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

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

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

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

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