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

Quality of Visual Studio Community code analysis with SAL annotations

本文关键字：SAL 注释 Studio Community 代码 Visual      更新时间：2023-10-16

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

在 C/C++ 中用于静态代码分析的 SAL 注释的概念对我来说似乎非常有用。以 MSDN 上错误实现的wmemcpy示例为例：了解 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 静态代码分析 - 它的可靠性如何？

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

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

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

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

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