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

Question

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

SAL annotations for static code analysis in C/C++ seems really useful to me. Take for example the wrongly implemented wmemcpy example on MSDN: 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 说 "a code analysis tool could catch the bug by analyzing this function alone"，这看起来不错，但问题是当我将这段代码粘贴到 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 注释是一种轻量级实现，可以在本地推理一个函数是否在做正确的事情，是否被错误地使用或相反。没有它们，您只能在整个程序的上下文中讨论错误的概念。有了它们，正如文档所说，就可以在本地说一个函数的行为是一个错误，你可以希望静态分析工具会找到它。

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

And if it's really quite bad: is this a known problem and are there maybe plans to improve this type of analysis?

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

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

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

Quality of Visual Studio Community code analysis with SAL annotations

c++

visual-studio-2017

static-analysis

sal