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行中添加以下选项。