ITADN
goblint/analyzer
README.md
以下内容由 AI 翻译,如有问题请点此提交 issue 反馈

Goblint

GitHub release status opam package status Zenodo DOI

locked workflow status unlocked workflow status Coverage Status docker workflow status Documentation Status project chat

文档可在 Read the DocsGitHub 上浏览。

安装

无论是使用最新版本的 Goblint 还是对其进行开发,最佳方式都是克隆此仓库并从源码安装。 要对 Goblint 进行基准测试,请遵循 Read the Docs 上的基准测试指南

Linux

  1. Install opam 2.2 or newer.
  2. Make sure the following are installed: git, patch, m4, autoconf, libgmp-dev, libmpfr-dev and pkg-config.
  3. Run make setup to install OCaml and dependencies via opam.
  4. Run make to build Goblint itself.
  5. Run make install to install Goblint into the opam switch for usage via switch's PATH.
  6. Optional: See scripts/bash-completion.sh for setting up bash completion for Goblint arguments.

MacOS

  1. 使用 brew install gcc grep 安装 GCC(如果不想从源码构建,请先运行 xcode-select --install)。Goblint 需要 GCC,而 macOS 的默认 cpp 是 Clang,无法使用。
  2. 仅适用于 M1 (ARM64) 处理器:homebrew 的安装位置已从 /usr/local/ 更改为 /opt/homebrew/。为了让包找到其依赖项,请执行 sudo ln -s /opt/homebrew/{include,lib} /usr/local/
  3. 继续使用 Linux 说明(brew 中 patchlibgmp-devlibmpfr-dev 的公式分别为 gpatchgmpmpfr)。

Windows

  1. 安装 WSL2。Goblint 与 WSL1 不兼容。
  2. 在 WSL 中继续使用 Linux 说明。

其他

  • opam。安装 opam 并运行 opam install goblint
  • devcontainer 在 VS Code 中选择 "Reopen in Container",并使用 devcontainer 中的 Linux 说明继续执行 make
  • Docker (GitHub Container Registry)。运行 docker pull ghcr.io/goblint/analyzer:latest(或 :nightly)。
  • Docker (repository)。 克隆并运行 docker build -t goblint .
  • Vagrant。 克隆并运行 vagrant up && vagrant ssh

运行

为了确认构建成功,您可以尝试按以下方式运行 Goblint:

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

为了确认安装到 opam switch 成功,您可以尝试按以下方式运行 Goblint:

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

为了确认 Docker 容器运行成功,您可以尝试按以下方式运行 Goblint:

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

如果从 GitHub Container Registry 拉取,请使用容器名称 ghcr.io/goblint/analyzer:latest(或 :nightly)代替。

有关更多信息,请参阅 documentation

致谢

Goblint 的工作部分由 Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 PUMA, 378803395/2428 ConVeY)、ARTEMIS Joint Undertaking (269335 MBAT)、ITEA3 项目 14014 ASSUME、格鲁吉亚 Shota Rustaveli 国家科学基金会 FR-21-7973、爱沙尼亚研究委员会(IUT2-1PSG61)以及爱沙尼亚信息技术卓越中心 (EXCITE) 支持,后者由欧洲区域发展基金资助。

我们还感谢 Zulip 为 Goblint 项目提供免费的 Zulip Cloud Standard 托管服务。Zulip 是一款开源的现代团队聊天应用,旨在保持实时和异步对话的有序进行。