clam下載 - clam源代碼下載

clam

其他類別

1.0.0

下載

蛤：llvm前端的螃蟹

CLAM是一種基於抽象解釋的靜態分析儀，它基於Crab庫計算LLVM比特碼的歸納不變。該分支支持LLVM 14。

可用的文檔可以在Clam Wiki和Crab Wiki中找到。

Docker

您可以使用命令從Docker Hub（每晚構建）獲得CLAM：

 docker pull seahorn/clam-llvm14:nightly

要求

Clam用C ++編寫，並大量使用Boost庫。主要要求是：

現代C ++編譯器支持C ++ 14
Boost> = 1.65
GMP
mpfr（僅當-DCRAB_USE_APRON=ON or或-DCRAB_USE_ELINA=ON ）
flint（僅當-DCRAB_USE_PPLITE=ON ）
python> = 3.6

在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

測試

測試基礎架構取決於幾個Python軟件包。要運行測試，您需要安裝lit和OutputCheck ：

 pip3 install lit
 pip3 install OutputCheck

彙編和安裝

基本彙編步驟是：

 1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR ../
3. cmake --build . --target crab && cmake ..   
4. cmake --build . --target extra && cmake ..                  
5. cmake --build . --target install

第2行的命令將嘗試從標準路徑找到LLVM 14。如果將LLVM 14安裝在非標準路徑中，則添加選項-DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm到第2行。第3行的命令將下載螃蟹並從源頭編譯。蛤使用通過第4行中的extra目標安裝的兩個外部組件。這些組件是：

SEA-DSA是用於翻譯LLVM記憶說明的堆分析。詳細信息可以在這里和這裡找到。
LLVM-Seahorn提供了LLVM組件的專門版本，以使其更適合驗證。 llvm-seahorn是可選的，但建議使用。

盒子/圍裙/Elina/Pplite域需要第三方庫。為了避免對那些對這些域不感興趣的用戶的負擔，庫的安裝是可選的。

如果要使用框域，請添加-DCRAB_USE_LDD=ON Option。
如果要使用圍裙庫域，請添加-DCRAB_USE_APRON=ON Option。
如果要使用Elina庫域，請添加-DCRAB_USE_ELINA=ON Option。
如果要使用pplite庫域，請添加-DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON Options。

重要的是：圍裙和Elina目前不兼容，因此您不能同時啟用-DCRAB_USE_APRON=ON和-DCRAB_USE_ELINA=ON同時。

例如，安裝帶有盒子和圍裙的蛤lam：

 1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..                
5. cmake --build . --target ldd && cmake ..
6. cmake --build . --target apron && cmake ..             
7. cmake --build . --target install

例如，第5行和第6行將分別下載，編譯和安裝框和圍裙庫。如果您已經在計算機中編譯並安裝了這些庫，則在第5和6行中跳過命令，並在第2行中添加以下選項。