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