我可以輕鬆地從靜態分析中排除一些合約嗎？

我知道靜態分析器無法證明某些合約。我可以從整個函數中排除特定類型的違反合同的錯誤，但這太寬泛了。我可以通過使用baseline.xml功能排除某些違規錯誤，但在團隊環境中進行審計或記錄基本上是不可能的。我可以輕鬆地從靜態分析中排除一些合約嗎？

總之，是有可能做這樣的事情

Contract.Requires(DoesHalt() == true, ExcludeFromStaticAnalysis=true);

也有似乎是靜態分析死角的第三方庫取得了一定的合同。我想禁用它們進行靜態分析。一個最喜歡的例子是一個.NET圖庫的契約。指定圖中哪個頂點開始搜索的深度優先搜索函數的參數具有要求頂點是圖的成員的Contract.Requires。明智的合同，甚至值得在調試版本中執行，但距離靜態證明很遠。然而，每次我使用深度優先搜索時，我都必須找到一種方法來忽略靜態違規。（它不能用Contract.Assume來解決）

如果沒有將可證明的東西與不可證實的東西進行分區的能力，我會發現靜態分析太簡單了，即使是乾淨的代碼基礎也是如此。

來源

2010-11-18 Sebastian Good

爲什麼你不能簡單地寫：「Contract.Requires（DoesHalt（）= true或AssumeTrueBecauseYouCantProveThis）」？ [其中AssumeTrueBecauseYouCantProvethis是一個靜態常量值「true」]。任何好的「證明者」都應該高興的是，這種分離的部分是非常正確的，並且在那個時候停止了合同檢查。 – 2010-12-21 00:27:09

因爲運行時檢查程序需要實際執行檢查。該檢查總是會與'||一起成功TRUE'。 – 2011-02-09 05:56:16

對於靜態分析，我知道沒有辦法做到這一點。運行時檢查程序有一個自定義的運行時間，這是可能的，但不適用於靜態檢查程序。

您可以做的是利用「基準功能」。這爲您提供了隱藏靜態檢查器在特定時間給您的所有警告的可能性。這些警告收集在XML文件中，直到您關閉基線功能。

這可以大大降低靜態檢查器的噪聲，爲現有的代碼庫。

來源

2010-11-29 20:03:33 koenmetsu

我可以輕鬆地從靜態分析中排除一些合約嗎？

回答

相關問題