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檔案，準備克隆。它也可以用於報告問題和提交拉請請求。