clam
1.0.0
La palourde est un analyseur statique basé sur l'interprétation abstraite qui calcule les invariants inductifs pour le code binaire LLVM basé sur la bibliothèque de crabe. Cette branche prend en charge LLVM 14.
La documentation disponible se trouve à la fois dans le wiki de palourdes et le wiki de crabe.
Vous pouvez obtenir la palourde de Docker Hub (construit par la nuit) en utilisant la commande:
docker pull seahorn/clam-llvm14:nightly
La palourde est écrite en C ++ et utilise fortement la bibliothèque Boost. Les principales exigences sont:
-DCRAB_USE_APRON=ON ou -DCRAB_USE_ELINA=ON )-DCRAB_USE_PPLITE=ON )Dans Linux, vous pouvez installer des exigences en tapant les commandes:
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
Le test de l'infrastructure dépend de plusieurs packages Python. Pour exécuter des tests, vous devez installer lit et OutputCheck :
pip3 install lit
pip3 install OutputCheck
Les étapes de compilation de base sont:
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
La commande de la ligne 2 essaiera de trouver LLVM 14 à partir de chemins standard. Si vous avez installé LLVM 14 dans un chemin non standard, ajoutez l'option -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm à la ligne 2. La commande de la ligne 3 téléchargera le crabe et le compile à partir de sources. Clam utilise deux composants externes installés via la cible extra à la ligne 4. Ces composants sont:
SEA-DSA est l'analyse du tas utilisé pour traduire les instructions de mémoire LLVM. Les détails peuvent être trouvés ici et ici.
LLVM-Seahorn fournit des versions spécialisées de composants LLVM pour les rendre plus provisoires pour la vérification. llvm-seahorn est facultatif mais recommandé.
Les domaines des boîtes / tabliers / elina / pplite nécessitent des bibliothèques tierces. Pour éviter le fardeau pour les utilisateurs qui ne sont pas intéressés par ces domaines, l'installation des bibliothèques est facultative.
Si vous souhaitez utiliser le domaine des boîtes, ajoutez -DCRAB_USE_LDD=ON l'option.
Si vous souhaitez utiliser les domaines de la bibliothèque de tabliers, ajoutez -DCRAB_USE_APRON=ON l'option.
Si vous souhaitez utiliser les domaines de la bibliothèque Elina, ajoutez -DCRAB_USE_ELINA=ON l'option.
Si vous souhaitez utiliser les domaines de la bibliothèque pplite, ajoutez -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON les options.
Important: Apron et Elina ne sont actuellement pas compatibles, vous ne pouvez donc pas activer -DCRAB_USE_APRON=ON et -DCRAB_USE_ELINA=ON en même temps.
Par exemple, pour installer la palourde avec des boîtes et un tablier:
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
Par exemple, les lignes 5 et 6 téléchargeront, compileront et installeront respectivement les boîtes et les bibliothèques de tabliers. Si vous avez déjà compilé et installé ces bibliothèques dans votre machine, sautez les commandes aux lignes 5 et 6 et ajoutez les options suivantes à la ligne 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 Pour exécuter certains tests de régression:
cmake --build . --target test-simple
Clam fournit un script Python appelé clam.py (situé à $DIR/bin où $DIR est le répertoire où la palourde a été installée) pour interagir avec les utilisateurs. La commande la plus simple est clam.py test.c Tapez clam.py --help pour toutes les options et lisez notre wiki.
