clam
1.0.0
O molusco é um analisador estático abstrato baseado em interpretação que calcula invariantes indutivos para o código de bits LLVM com base na biblioteca do caranguejo. Esta filial suporta LLVM 14.
A documentação disponível pode ser encontrada tanto no Wiki do CLAM quanto no Wiki de caranguejo.
Você pode obter molusco do Docker Hub (construído noturno) usando o comando:
docker pull seahorn/clam-llvm14:nightly
O molusco é escrito em C ++ e usa fortemente a biblioteca Boost. Os principais requisitos são:
-DCRAB_USE_APRON=ON ou -DCRAB_USE_ELINA=ON )-DCRAB_USE_PPLITE=ON )No Linux, você pode instalar requisitos digitando os comandos:
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
A infraestrutura de teste depende de vários pacotes Python. Para executar os testes, você precisa instalar lit e OutputCheck :
pip3 install lit
pip3 install OutputCheck
As etapas básicas de compilação são:
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
O comando na linha 2 tentará encontrar LLVM 14 a partir de caminhos padrão. Se você instalou o LLVM 14 em um caminho fora do padrão, adicione a opção -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm na linha 2. O comando na linha 3 fará o download do caranguejo e o compilará de fontes. O molusco usa dois componentes externos instalados através do alvo extra na linha 4. Esses componentes são:
SEA-DSA é a análise de heap usada para traduzir instruções de memória LLVM. Os detalhes podem ser encontrados aqui e aqui.
O LLVM-Seahorn fornece versões especializadas dos componentes LLVM para torná-los mais passíveis de verificação. llvm-seahorn é opcional, mas recomendado.
Os domínios de caixas/avental/elina/pplite requerem bibliotecas de terceiros. Para evitar o ônus dos usuários que não estão interessados nesses domínios, a instalação das bibliotecas é opcional.
Se você deseja usar o domínio das caixas, adicione -DCRAB_USE_LDD=ON opção.
Se você deseja usar os domínios da biblioteca de avental, adicione -DCRAB_USE_APRON=ON opção.
Se você deseja usar os domínios da biblioteca Elina, adicione -DCRAB_USE_ELINA=ON opção.
Se você deseja usar os domínios da biblioteca Pplite, adicione -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON opções.
IMPORTANTE: Apron e Elina atualmente não são compatíveis, portanto você não pode ativar -DCRAB_USE_APRON=ON e -DCRAB_USE_ELINA=ON ao mesmo tempo.
Por exemplo, para instalar moluscos com caixas e avental:
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
Por exemplo, as linhas 5 e 6 baixam, compilam e instalam as caixas e as bibliotecas de avental, respectivamente. Se você já compilou e instalou essas bibliotecas em sua máquina, pule os comandos na linha 5 e 6 e adicione as seguintes opções na linha 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 Para executar alguns testes de regressão:
cmake --build . --target test-simple
O CLAM fornece um script python chamado clam.py (localizado em $DIR/bin , onde $DIR é o diretório onde o molusco foi instalado) para interagir com os usuários. O comando mais simples é clam.py test.c Digite clam.py --help para todas as opções e leia nosso wiki.
