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 。
如果您的项目使用cmake ，则只需要添加项目的CMakeLists.txt ：
add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})
然后将您的可执行文件与${CRAB_LIBS}链接
如果您的项目使用make ，请阅读此样本Makefile。
