clam
1.0.0
Clam ist ein abstrakter interpretationsbasierter statischer Analysator, der induktive Invarianten für LLVM-Bitcode basierend auf der Krabbenbibliothek berechnet. Dieser Zweig unterstützt LLVM 14.
Die verfügbare Dokumentation finden Sie sowohl im Muschel Wiki als auch in Crab Wiki.
Mit dem Befehl können Sie Muscheln von Docker Hub (nächtlich gebaut) erhalten:
docker pull seahorn/clam-llvm14:nightly
Clam ist in C ++ geschrieben und verwendet die Boost -Bibliothek stark. Die Hauptanforderungen sind:
-DCRAB_USE_APRON=ON oder -DCRAB_USE_ELINA=ON )-DCRAB_USE_PPLITE=ON )In Linux können Sie die Anforderungen installieren, die die Befehle eingeben:
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
Die Testinfrastruktur hängt von mehreren Python -Paketen ab. Um Tests auszuführen, müssen Sie lit und OutputCheck installieren:
pip3 install lit
pip3 install OutputCheck
Die grundlegenden Zusammenstellungsschritte sind:
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
Der Befehl in Zeile 2 versucht, LLVM 14 von Standardpfaden zu finden. Wenn Sie LLVM 14 in einem nicht standardmäßigen Pfad installiert haben, fügen Sie die Option -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm zu Zeile 2 hinzu. Der Befehl in Zeile 3 wird Crab herunterladen und aus den Quellen kompilieren. Clam verwendet zwei externe Komponenten, die über das extra Ziel in Zeile 4 installiert sind. Diese Komponenten sind:
SEA-DSA ist die Heap-Analyse, die zur Übersetzung von LLVM-Speicheranweisungen verwendet wird. Details finden Sie hier und hier.
LLVM-Seahorn bietet spezielle Versionen von LLVM-Komponenten, damit sie für die Überprüfung zugänglicher werden können. llvm-seahorn ist optional, aber Hightly empfohlen.
Die Kästchen/Schürze/Elina/PPLite-Domänen erfordern Bibliotheken von Drittanbietern. Um die Belastung für Benutzer zu vermeiden, die sich nicht für diese Domänen interessieren, ist die Installation der Bibliotheken optional.
Wenn Sie die Kästchen -Domäne verwenden möchten, fügen Sie die Option -DCRAB_USE_LDD=ON .
Wenn Sie die Domänen der Apron -Bibliothek verwenden möchten, fügen Sie die Option -DCRAB_USE_APRON=ON .
Wenn Sie die Elina -Bibliotheksdomänen verwenden möchten, fügen Sie -DCRAB_USE_ELINA=ON .
Wenn Sie die PPLite -Bibliotheksdomänen verwenden möchten, fügen Sie -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON Optionen hinzu.
Wichtig: Schürze und Elina sind derzeit nicht kompatibel, sodass Sie nicht gleichzeitig -DCRAB_USE_APRON=ON und -DCRAB_USE_ELINA=ON aktivieren können.
Zum Beispiel, um Muscheln mit Kisten und Schürze zu installieren:
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
Zum Beispiel werden die Zeilen 5 und 6 die Boxen bzw. Schürze -Bibliotheken herunterladen, kompilieren und installieren. Wenn Sie diese Bibliotheken bereits in Ihrem Computer kompiliert und installiert haben, überspringen Sie die Befehle in Zeile 5 und 6 und fügen Sie die folgenden Optionen in Zeile 2 hinzu.
-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 Einige Regressionstests durchführen:
cmake --build . --target test-simple
Clam bietet ein Python -Skript namens clam.py (das sich bei $DIR/bin befindet, in dem $DIR das Verzeichnis ist, in dem Clam installiert wurde) mit den Benutzern zu interagieren. Der einfachste Befehl ist clam.py test.c Geben Sie clam.py --help für alle Optionen ein und lesen Sie unser Wiki.
