c# - 使用代码契约，为什么 ccrewrite 需要访问每个运行时依赖项？

Question

我正在尝试使用代码合同，但遇到了一个阻碍我的问题。将 Contract Reference Assembly 设置为 Build 时，ccrewrite 在尝试访问由直接引用的程序集间接引用的程序集时出错。构建解决方案不需要这些间接程序集，所以我想知道为什么代码合同需要它们？此外，有没有办法解决这个问题，而不必提供所有运行时依赖项作为构建的一部分？

Answer 1

重写器查看引用程序集的方法体以提取合同（C# 编译器从不这样做）。结果，重写器经常追逐比 C# 更多的依赖项，这是您遇到的问题。

有两种方法可以解决这个问题。

1. 在可以找到所需库的目录中添加额外的路径（在合约库路径选项中）。这是首选方法
2. 作为最后的手段，您可以将选项添加-ignoreMetadataErrors到运行时合约选项。请注意，这是危险的。如果重写器确实需要引用代码的某些方面来创建正确的 IL，那么您最终可能会得到不正确的 IL。为了防止这种情况，请在结果位上使用 peverify。

希望这可以帮助。

Answer 2

我假设 ccrewrite 正在尝试遍历依赖链以分析它的前置/后置条件等。如果程序集被您反过来引用的程序集引用，那么它们将是您的程序运行所必需的，因此 ccrewrite 只是在执行在实际运行程序之前进行常规分析。

那是基于使用 JML；我自己才刚刚开始研究 .NET 代码合同。但我相信这两种工具的运作原理大致相同。