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

Question

我希望这个问题不超出SO的范围; 如果是(对不起那种情况),请告诉我它属于哪里,我会尝试将它移到那里.

用于C/C++中静态代码分析的SAL注释的概念对我来说似乎非常有用.以MSDNwmemcpy上错误实现的示例为例:了解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)..)

这应该产生警告(至少根据另一个例子回答什么是SAL(来源标注语言)的目的是什么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_和没有_In_或_Inout_因此这个警告不会在这种情况下才有意义.

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

如果它真的非常糟糕:这是一个已知的问题,是否有可能计划改进这种类型的分析？

相关:visual studio 2013静态代码分析 - 它有多可靠？

Answer 1

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

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

如果情况确实很糟糕：这是一个已知问题吗？是否有计划改进此类分析？

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

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