function
1.0.0
기능은 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
Dune : OCAML 빌드 시스템
opam install dune
ounit
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
분석기는 속성을 성공적으로 증명할 수있는 경우에 대답합니다. 그렇지 않으면 알 수없는 대답입니다.
함수는 다음 속성을 분석 할 수 있습니다.
종료를 확인하려면 다음 호출 패턴으로 분석기에 전화하십시오.
./function <file> -termination [options]
다음 통화 패턴은 속성 또는 재발 속성을 보장하는 데 사용할 수 있습니다.
./function <file> -guarantee <property_file> [options]
./function <file> -recurrence <property_file> [options]
여기서 "property_file"은 보증 또는 재발 속성을 포함하는 파일의 경로입니다.
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
