analyzer

Gobele

La documentation peut être parcourue sur Lire les documents ou GitHub.

Installation

À la fois pour utiliser une version à jour de Goblint ou le développer, la meilleure façon est d'installer à partir de la source en clonage ce référentiel. Pour l'analyse comparative de gobelint, veuillez suivre le guide d'analyse comparative sur les documents.

Linux

1. Installer OPAM.
2. Assurez-vous que les éléments suivants sont installés: git , patch , m4 , autoconf , libgmp-dev , libmpfr-dev et pkg-config .
3. Exécutez make setup pour installer OCAML et les dépendances via OPAM.
4. Run make pour construire gobelint lui-même.
5. Exécutez make install pour installer Goblint dans le commutateur OPAM pour utiliser le PATH du commutateur.
6. Facultatif: voir scripts/bash-completion.sh pour configurer l'achèvement de bash pour les arguments gobelint.

Macos

1. Installez GCC avec brew install gcc grep (First Exécutez xcode-select --install si vous ne voulez pas le construire à partir de Source). Goblint nécessite GCC tandis que cpp par défaut de MacOS est Clang, ce qui ne fonctionnera pas.
2. Seulement pour le processeur M1 (ARM64): Homebrew a modifié son emplacement d'installation à partir de /usr/local/ to /opt/homebrew/ . Pour les packages pour trouver leurs dépendances, exécutez sudo ln -s /opt/homebrew/{include,lib} /usr/local/ .
3. Continuez à utiliser les instructions Linux (les formules dans Brew for patch , libgmp-dev , libmpfr-dev sont respectivement gpatch , gmp , mpfr ).

Fenêtre

1. Installez WSL2. Goblint n'est pas compatible avec WSL1.
2. Continuez à utiliser les instructions Linux dans WSL.

Autre

• Opam . Installez OPAM et exécutez opam install goblint .
• DevContainer. Sélectionnez "Rouvrir dans le conteneur" dans VS Code et continuez avec make instructions Linux dans DevContainer.
• Docker (github Container Registry) . Run docker pull ghcr.io/goblint/analyzer:latest (ou :nightly ).
• Docker (référentiel). Clone et exécuter docker build -t goblint . .
• Vagabond. Clone et exécuter vagrant up && vagrant ssh .

En cours d'exécution

Pour confirmer que le bâtiment a fonctionné, vous pouvez essayer de faire fonctionner Goblint comme suit:

 ./goblint tests/regression/04-mutex/01-simple_rc.c

Pour confirmer que l'installation dans l'interrupteur OPAM a fonctionné, vous pouvez essayer d'exécuter Goblint comme suit:

 goblint tests/regression/04-mutex/01-simple_rc.c

Pour confirmer que le conteneur Docker a fonctionné, vous pouvez essayer d'exécuter Goblint comme suit:

 docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c

Si vous êtes tiré du registre des conteneurs GitHub, utilisez le nom de conteneur ghcr.io/goblint/analyzer:latest (ou :nightly ) à la place.

Pour plus d'informations, voir la documentation.

Remerciements

Les travaux sur Goblint ont été soutenus en partie par Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 PUMA, 378803395/2428 Convey), Artemis Joint Enverating (269335 MBAT), Ite3 Project 14014, Assume, The Shota Rustaveli Le Conseil de recherche estonien (IUT2-1, PSG61) et le Centre d'excellence estonien (excite), financé par le Fonds européen de développement régional.

Nous remercions également Zulip d'avoir fourni un hébergement standard cloud Zulip gratuit pour le projet Goblint. Zulip est une application de chat d'équipe moderne open source conçue pour garder les conversations en direct et asynchrones organisées.