function

功能

功能是一種研究原型靜態分析儀，旨在證明C程序的條件終止和有條件的保證和復發性能。該工具會自動通過抽象解釋來注入分段定義的排名函數和足夠的終止，保證和復發屬性的前提。

開發了函數來實施和測試文章中描述的分析方法和摘要域：

 N. Courant, C. Urban. Precise Widening Operators for Proving Termination by Abstract Interpretation.

C. Urban, A. Miné. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation.
In Proc. 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015). 

C. Urban, A. Miné. A Decision Tree Abstract Domain for Proving Conditional Termination.
In Proc. 21st International Static Analysis Symposium (SAS 2014).

C. Urban, A. Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions.
In Proc. 23rd European Symposium on Programming (ESOP 2014).

C. Urban. The Abstract Domain of Segmented Ranking Functions.
In Proc. 20th International Static Analysis Symposium (SAS 2013).

函數的主要網站是：http：//www.di.ens.fr/~urban/function.html

作者

 Caterina Urban, ETH Zurich, [email protected] 

貢獻者

 Naïm Moussaoui Remil, École Normale Supérieure
Samuel Ueltschi, ETH Zurich
Nathanaëlle Courant, École Normale Supérieure

安裝

功能需要以下應用程序和庫：

• OCAML

   (sudo) apt-get install ocaml-interp
  

• Findlib

   (sudo) apt-get install ocaml-findlib
  

• Menhir：LR（1）解析器發電機

   (sudo) apt-get install menhir
  

• OPAM：https：//opam.ocaml.org/doc/install.html

   (sudo) apt-get install opam
  

• 沙丘：OCAML構建系統

   opam install dune
  

• 盎司

   opam install ounit
  

• 圍裙：數字抽象域庫

   opam install apron
  

• Zarith：任意精確整數操作

   opam install zarith
  

編譯功能

一旦安裝了所有必需的庫，就可以使用“ Dune”來編譯功能：

 dune build

這將在項目目錄中生成命令行程序“函數”。

另外，“ OcamlBuild”可用於使用以下命令來構建函數：

 ocamlbuild ml_float.o Main.native -use-ocamlfind -use-menhir -pkgs 'apron,gmp,oUnit,zarith' -I utils -I banal -I domains -I frontend -I cfgfrontend -I main -libs boxMPQ,octD,polkaMPQ,str,zarith -lflags banal/ml_float.o

用法

可以使用以下呼叫模式調用命令行分析儀：

 ./function <file> <analysis> [options] 

其中“文件”是要分析的C文件的路徑和“分析”要執行的分析的類型。

該分析儀首先執行遠程可及性分析，然後進行向後分析，以在輸入點找到分段定義的排名函數和足夠的前提條件，以使程序滿足給定的分析屬性。

識別以下一般命令行選項（顯示其默認值）：

 -main main                         set the analyzer entry point (defaults to main)
 -domain boxes|octagons|polyhedra   set the abstract domain (defaults to boxes)
 -joinfwd 2                         set the widening delay in forward analysis
 -joinbwd 2                         set the widening delay in backward analysis
 -meetbwd 2			                set the dual widening delay in backward analysis
 -ordinals 2                        set the maximum ordinal value for the ranking functions
 -refine            			    reduces the backward analysis to the reachabile states

分析儀回答為True，以防它可以成功證明該屬性。否則，它回答未知。

功能可以分析以下屬性：

• 終止
• 保證 /復發
• 計算-Tree-Logic（CTL）

終止

要檢查終止，請致電以下呼叫模式致電分析器：

 ./function <file> -termination [options]

保證 /復發

以下呼叫模式可用於保證屬性或複發屬性：

 ./function <file> -guarantee <property_file> [options]
./function <file> -recurrence <property_file> [options] 

其中“ property_file”是包含保證或複發屬性的文件的路徑。

CTL

CTL屬性可以使用以下呼叫模式進行分析：

 ./function <file> -ctl <property> [options]

其中“屬性”是要分析的CTL屬性。

CTL分析存在以下其他命令行選項：（顯示其默認值）：

 -precondition true                 a precondition that is assumed to hold at the start of the program
 -noinline			                disable inlining of function calls
 -ast                               run the analysis on the abstract-syntax-tree instead of the control-flow-graph,
                                    note that in that case function calls and goto/break/continue are not supported
 -dot                               print out control-flow-graph and decision trees in graphviz dot format