crab
1.0.0
CRAB是基於抽象解釋的C ++庫進行構建程序靜態分析。 CRAB提供了豐富的抽象域，基於Kleene的FixPoint求解器，以及不同的分析，例如數據流，封閉式和後退。螃蟹的設計非常模塊化，因此很容易插入新的抽象域和求解器或構建新的分析。
螃蟹抽象域可以推理內存內容，類似C的數組和數值屬性。螃蟹使用流行數值域的有效實現，例如區域和八塊以及新穎的域，例如關於符號術語（又稱未解釋的函數）。螃蟹還使用有效的環境圖實現了流行的非關係域，例如間隔或一致性，並允許通過標準減少的產品結構組合任意域。 CRAB還提供了非凸線域，例如基於線性決策圖的專門分離間隔，稱為框，以及更一般的價值分配策略，該策略將任意域提升到對其脫節完成的過度評價。除了這些域，所有這些領域都由螃蟹作者開發，螃蟹庫還集成了流行的抽象域庫，例如圍裙，Elina和Pplite。
螃蟹提供了最新的交織固定點求解器，該解決方案使用Bourdoncle的弱拓撲訂購來選擇一組延伸點。為了減輕擴大過程中的精確損失，CRAB實現了一些流行的技術，例如通過閾值擴大和lookahead拓寬。
CRAB提供了兩個不同的手術間分析的實現：一個自上而下的，具有紀念性術間分析，並支持遞歸呼叫，以及自下而上 +自上而下分析的混合體。最後但並非最不重要的一點是，CRAB還實施了更實驗性的向後分析，可用於計算必要的先決條件和/或減少錯誤警報的數量。
螃蟹不直接分析主流編程語言，而是分析了其自己的基於CFG的中間表示，稱為Crabir。 Crabir是三個地址的代碼，它是強烈鍵入的。在Crabir中，控制流是通過非確定性的GOTO指令來定義的。除了標準布爾和算術操作外，Crabir還提供特殊的假設和斷言聲明。前者可用於完善控制流，後者提供了一個簡單的機制來檢查用戶定義的屬性。儘管它具有簡單的設計，但Crabir還是足夠豐富的，可以代表LLVM等語言。
螃蟹正在積極發展。如果找到錯誤，請打開GitHub問題。帶有新功能的拉請求非常歡迎。可用的文檔可以在我們的Wiki中找到。如果您使用此庫，請引用本文。
| 視窗 | Ubuntu | OS X | 覆蓋範圍 |
|---|---|---|---|
| TBD |  | TBD |
可以使用Docker獲得所有測試的（夜間）預構建的螃蟹版本：
docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionic螃蟹用C ++編寫，並依靠Boost庫。主要要求是：
-DCRAB_USE_APRON=ON或-DCRAB_USE_ELINA=ON ）-DCRAB_USE_PPLITE=ON ）在Linux中，您可以安裝鍵入命令的要求：
sudo apt-get install libboost-all-dev libboost-program-options-dev
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev
sudo apt-get install libflint-dev
要安裝螃蟹，請輸入：
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
3. cmake --build . --target install
tests目錄包含許多示例，說明瞭如何使用不同的分析和抽象域來構建用Crabir編寫的程序進行計算。要編譯這些測試，添加選項-DCRAB_ENABLE_TESTS=ON 2行2。
然後，例如，運行test1 ：
build/test-bin/test1
盒子/圍裙/Elina/Pplite域需要第三方庫。為了避免對那些對這些域不感興趣的用戶的負擔，庫的安裝是可選的。
如果要使用框域，請添加-DCRAB_USE_LDD=ON Option。
如果要使用圍裙庫域，請添加-DCRAB_USE_APRON=ON Option。
如果要使用Elina庫域，請添加-DCRAB_USE_ELINA=ON Option。
如果要使用pplite庫域，請添加-DCRAB_USE_PPLITE=ON Option。
重要的是：圍裙和Elina目前不兼容，因此您不能同時啟用-DCRAB_USE_APRON=ON和-DCRAB_USE_ELINA=ON同時。
例如，要安裝帶有盒子和圍裙的螃蟹，請輸入：
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target ldd && cmake ..
4. cmake --build . --target apron && cmake ..
5. cmake --build . --target install
第3和4行將分別下載，編譯和安裝框和圍裙域。如果您想使用elina或pplite ，請用Elina或Pplite在第4行中替換apron 。如果您已經在計算機中編譯並安裝了這些庫，則在第3和4行中跳過命令，並在第2行中添加以下選項。
-DAPRON_ROOT=$APRON_INSTALL_DIR-DELINA_ROOT=$ELINA_INSTALL_DIR-DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR-DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR要在您的C ++應用中包括Crab，您需要：
包括位於$INSTALL_DIR/crab/include的C ++標頭文件，並
將您的應用程序與安裝在$INSTALL_DIR/crab/lib中的螃蟹庫鏈接。
如果您使用盒子/圍裙/Elina/pplite編譯，則還需要包括$INSTALL_DIR/EXT/include and $INSTALL_DIR/EXT/lib ，其中EXT=apron|elina|ldd|pplite pplite 。
如果您的項目使用cmake ，則只需要添加項目的CMakeLists.txt ：
add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})
然後將您的可執行文件與${CRAB_LIBS}鏈接
如果您的項目使用make ，請閱讀此樣本Makefile。
