我可以轻松地从静态分析中排除一些合约吗？
问题描述：
我知道静态分析器无法证明某些合约。我可以从整个函数中排除特定类型的违反合同的错误，但这太宽泛了。我可以通过使用baseline.xml功能排除某些违规错误，但在团队环境中进行审计或记录基本上是不可能的。我可以轻松地从静态分析中排除一些合约吗？
总之，是有可能做这样的事情
Contract.Requires(DoesHalt() == true, ExcludeFromStaticAnalysis=true);
也有似乎是静态分析死角的第三方库取得了一定的合同。我想禁用它们进行静态分析。一个最喜欢的例子是一个.NET图库的契约。指定图中哪个顶点开始搜索的深度优先搜索函数的参数具有要求顶点是图的成员的Contract.Requires。明智的合同，甚至值得在调试版本中执行，但距离静态证明很远。然而，每次我使用深度优先搜索时，我都必须找到一种方法来忽略静态违规。 （它不能用Contract.Assume来解决）
如果没有将可证明的东西与不可证实的东西进行分区的能力，我会发现静态分析太简单了，即使是干净的代码基础也是如此。
答
对于静态分析，我知道没有办法做到这一点。运行时检查程序有一个自定义的运行时间，这是可能的，但不适用于静态检查程序。
您可以做的是利用“基准功能”。这为您提供了隐藏静态检查器在特定时间给您的所有警告的可能性。这些警告收集在XML文件中，直到您关闭基线功能。
这可以大大降低静态检查器的噪声，为现有的代码库。
为什么你不能简单地写：“Contract.Requires（DoesHalt（）= true或AssumeTrueBecauseYouCantProveThis）”？ [其中AssumeTrueBecauseYouCantProvethis是一个静态常量值“true”]。任何好的“证明者”都应该高兴的是，这种分离的部分是非常正确的，并且在那个时候停止了合同检查。 – 2010-12-21 00:27:09
因为运行时检查程序需要实际执行检查。该检查总是会与'||一起成功TRUE'。 – 2011-02-09 05:56:16