热门搜索:

seahorn/clam-llvm14

seahorn

基于抽象解释的LLVM 14静态分析工具，用于程序分析与验证（https://github.com/seahorn/clam）

下载次数: 0状态：社区镜像维护者：seahorn仓库类型：镜像最近更新：1 个月前

使用轩辕镜像，把时间还给真正重要的事。点击查看

中文简介

标签下载

镜像标签列表与下载命令

使用轩辕镜像，把时间还给真正重要的事。点击查看

Clam Docker镜像文档

镜像概述

Clam Docker镜像是基于seahorn/clam项目构建的静态分析工具容器化版本，实现了基于抽象解释技术的程序分析能力，专门针对LLVM 14中间表示(IR)格式的代码进行静态分析与验证。

核心功能与特性

抽象解释技术：采用抽象解释理论进行静态程序分析，能够在不执行程序的情况下推断程序行为
LLVM 14支持：完全兼容LLVM 14中间表示(IR)格式，可分析LLVM 14编译生成的.ll或.bc文件
程序验证能力：提供程序正确性验证、不变式推断和潜在缺陷检测功能
轻量级部署：容器化封装，无需复杂依赖配置，可直接集成到CI/CD流程

使用场景与适用范围

编译器优化验证与正确性检查
安全关键软件的漏洞静态检测
程序不变式自动推断与验证
学术研究中的静态分析算法实现与测试
教学环境中的程序分析技术实践

使用方法与配置说明

基本使用方法

通过docker run命令运行容器，挂载本地代码目录进行分析：

bash
# 基本分析命令
docker run --rm -v /本地代码路径:/workspace seahorn/clam:latest clam --input /workspace/目标程序.ll

# 查看帮助信息
docker run --rm seahorn/clam:latest clam --help

常用参数说明

--input <file>: 指定待分析的LLVM IR文件路径（.ll或.bc格式）
--domain <domain>: 指定抽象域（如interval、octagon等）
--entry <function>: 指定分析入口函数（默认为main函数）
--output <file>: 指定分析结果输出文件路径
--verbose: 启用详细输出模式

示例：分析LLVM IR文件

准备LLVM 14生成的IR文件（例如test.ll）
执行分析命令：

bash
docker run --rm -v $(pwd):/workspace seahorn/clam:latest clam --input /workspace/test.ll --domain interval --verbose

注意事项

确保输入文件为LLVM 14兼容的IR格式，可通过llvm-as-14工具生成
复杂程序分析可能需要根据代码特性调整抽象域参数以平衡分析精度与性能
分析结果将显示在标准输出或指定的输出文件中，包含程序不变式和潜在问题报告

镜像拉取方式

您可以使用以下命令拉取该镜像。请将 <标签> 替换为具体的标签版本。如需查看所有可用标签版本，请访问标签列表页面。

轩辕镜像加速拉取命令点我查看更多 clam-llvm14 镜像标签

docker pull docker.xuanyuan.run/seahorn/clam-llvm14:<标签>

使用方法：

DockerHub 原生拉取命令

docker pull seahorn/clam-llvm14:<标签>

轩辕镜像配置手册

探索更多轩辕镜像的使用方法，找到最适合您系统的配置方式

Docker 配置

登录仓库拉取

通过 Docker 登录认证访问私有仓库

专属域名拉取

无需登录使用专属域名

K8s Containerd

Kubernetes 集群配置 Containerd

K3s

K3s 轻量级 Kubernetes 镜像加速

Dev Containers

VS Code Dev Containers 配置

Podman

Podman 容器引擎配置

Singularity/Apptainer

HPC 科学计算容器配置

其他仓库配置

ghcr、Quay、nvcr 等镜像仓库

Harbor 镜像源配置

Harbor Proxy Repository 对接专属域名

Portainer 镜像源配置

Portainer Registries 加速拉取

Nexus 镜像源配置

Nexus3 Docker Proxy 内网缓存

系统配置

Linux

在 Linux 系统配置镜像服务

Windows/Mac

在 Docker Desktop 配置镜像

MacOS OrbStack

MacOS OrbStack 容器配置

Docker Compose

Docker Compose 项目配置

NAS 设备

群晖

Synology 群晖 NAS 配置

飞牛

飞牛 fnOS 系统配置镜像

绿联

绿联 NAS 系统配置镜像

威联通

QNAP 威联通 NAS 配置

极空间

极空间 NAS 系统配置服务

网络设备

爱快路由

爱快 iKuai 路由系统配置

宝塔面板

在宝塔面板一键配置镜像

需要其他帮助？请查看我们的常见问题Docker 镜像访问常见问题解答或提交工单

镜像拉取常见问题

使用与功能问题

配置了专属域名后，docker search 为什么会报错？

docker search 限制

Docker Hub 上有的镜像，为什么在轩辕镜像网站搜不到？

站内搜不到镜像

机器不能直连外网时，怎么用 docker save / load 迁镜像？

离线 save/load

docker pull 拉插件报错（plugin v1+json）怎么办？

插件要用 plugin install

WSL 里 Docker 拉镜像特别慢，怎么排查和优化？

WSL 拉取慢

轩辕镜像安全吗？如何用 digest 校验镜像没被篡改？

安全与 digest

第一次用轩辕镜像拉 Docker 镜像，要怎么登录和配置？

新手拉取配置

轩辕镜像合规吗？轩辕镜像的合规是怎么做的？

镜像合规机制

错误码与失败问题

docker pull 提示 manifest unknown 怎么办？

manifest unknown

docker pull 提示 no matching manifest 怎么办？

no matching manifest（架构）

镜像已拉取完成，却提示 invalid tar header 或 failed to register layer 怎么办？

invalid tar header（解压）

Docker pull 时 HTTPS / TLS 证书验证失败怎么办？

TLS 证书失败

Docker pull 时 DNS 解析超时或连不上仓库怎么办？

DNS 超时

docker 无法连接轩辕镜像域名怎么办？

域名连通性排查

Docker 拉取出现 410 Gone 怎么办？

410 Gone 排查

出现 402 或「流量用尽」提示怎么办？

402 与流量用尽

Docker 拉取提示 UNAUTHORIZED（401）怎么办？

401 认证失败

遇到 429 Too Many Requests（请求太频繁）怎么办？

429 限流

docker login 提示 Cannot autolaunch D-Bus，还算登录成功吗？

D-Bus 凭证提示

为什么会出现「单层超过 20GB」或 413，无法加速拉取？

413 与超大单层

账号 / 计费 / 权限

轩辕镜像免费版和专业版有什么区别？

免费版与专业版区别

轩辕镜像支持哪些 Docker 镜像仓库？

支持的镜像仓库

镜像拉取失败还会不会扣流量？

失败是否计费

麒麟 V10 / 统信 UOS 提示 KYSEC 权限不够怎么办？

KYSEC 拦截脚本

如何在轩辕镜像申请开具发票？

申请开票

怎么修改轩辕镜像的网站登录和仓库登录密码？

修改登录密码

如何注销轩辕镜像账户？要注意什么？

注销账户

配置与原理类

写了 registry-mirrors，为什么还是走官方或仍然报错？

mirrors 不生效

怎么用 docker tag 去掉镜像名里的轩辕域名前缀？

去掉域名前缀

如何拉取指定 CPU 架构的镜像（如 ARM64、AMD64）？

指定架构拉取

用轩辕镜像拉镜像时快时慢，常见原因有哪些？

拉取速度原因

查看全部问题→

用户好评

来自真实用户的反馈，见证轩辕镜像的优质服务

oldzhang

运维工程师

Linux服务器

"Docker访问体验非常流畅，大镜像也能快速完成下载。"