Frama C snapshot

Frama-C是一个平台，致力于分析C中编写的源代码。

注意：官方的Frama-C存储库现在在我们的Gitlab！

Frama-C已将其官方存储库转移到了我们的自主Gitlab实例中。

官方版本（从Frame-C 21开始）将不再在此处更新。

我们的gitlab也有每晚的快照！您现在可以访问以下网址：https：//git.frama-c.com/pub/frama-c/-/tree/master

官方Frama-C问题跟踪器现在在我们的GitLab：https：//git.frama-c.com/pub/frama-c/-/issues

您可以使用GITHUB登录（提示时选择“使用GitHub登录”）提交问题并提取请求。

在那里见！

协作平台

Frama-C在单个协作平台中收集了几种分析技术，该平台由内核组成，该内核提供了一组核心功能（例如，用于C程序的标准化AST）以及一组称为插件的分析仪。插件可以基于平台中其他插件计算的结果。

得益于这种方法，Frama-C提供了复杂的工具，包括：

• 基于抽象解释的分析仪，旨在验证缺乏运行时错误（ EVA ）；
• 基于最弱的先决条件演算（ WP ）的程序证明框架；
• 程序切片机（切片）；
• 验证时间（LTL）属性（ AORAï ）的工具；
• 运行时验证工具（ E-ACSL ）；
• 代码基础探索和依赖性分析的几种工具（来自影响，指标，发生，范围等）。

这些插件共享一种通用语言，并可以通过ACSL （ ANSI/ISO C规范语言）属性交换信息。插件也可以通过其API进行协作。

安装

有关安装OPAM/FRAMA-C的更多详细信息，请参见install.md。

Frama-C可通过OPAM（OPAM），OCAML软件包管理器获得。这是首选的安装方法。确保安装OPAM v2.0或更高版本。然后，以下命令序列应安装frama-c及其GUI：

 opam init
opam install depext
opam depext frama-c
opam install frama-c

Frama-C主要在Linux中开发，经常在MacOS（通过Homebrew）中进行测试，并偶尔在Windows上测试（通过Windows子系统的Linux）进行了测试。

用法

frama-c可以从命令行或图形接口运行。

简单用法

简单文件的建议用法是以下几行：

 frama-c file.c -<plugin> [options]
frama-c-gui file.c

其中-<plugin>是几个frama -c插件之一，例如-eva或-wp或-metrics等。插件也可以直接从GUI运行。

要列出所有插件，请运行：

 frama-c -plugins

每个插件都有一个help命令（ -<plugin>-help或-<plugin>-h ），可描述其几个选项。

最后，可以通过

 frama-c -kernel-help

复杂的方案

对于更复杂的用法方案（许多文件和目录，还有多个预处理指令），我们建议将Frama-C的用法分为两个部分：

1. 解析输入文件并将结果保存到文件；
2. 加载解析结果，然后运行分析或GUI。

解析通常涉及向C预处理器提供额外的参数，因此-cpp-extra-args选项通常很有用，如下示例：

 frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

然后将结果加载到frama-C中进行进一步分析或通过GUI检查：

 frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

进一步参考

• 可在用户和开发人员手册，frama-c档案和插件手册的链接
  http://frama-c.com/download.html

• Stackoverflow在frama-c标签上有几个问题，该标签受到Frama-C社区的几个成员的监控。

• Frama-C-Discuss邮件列表用于公告和一般讨论。

• 官方的错误跟踪系统可用于错误报告。

• Frama-C Wiki有一些有用的信息，尽管它不是完全最新的。

• Frama-C博客有几篇有关Frama-C的新发展以及有关C语言，未定义行为，浮点计算等的一般讨论的文章。

• GitHub快照存储库包含稳定的frama-c版本的.tar.gz档案，准备克隆。它也可以用于报告问题和提交拉请请求。