function

Fungsi

Fungsi adalah prototipe penelitian penganalisa statis yang dirancang untuk membuktikan penghentian bersyarat dan jaminan bersyarat dan sifat kekambuhan dari program C. Alat ini secara otomatis menyimpulkan fungsi peringkat yang ditentukan oleh piecewise dan prasyarat yang cukup untuk pengakhiran, jaminan dan sifat kekambuhan dengan cara interpretasi abstrak.

Fungsi dikembangkan untuk mengimplementasikan dan menguji metode analisis dan domain abstrak yang dijelaskan dalam artikel:

 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).

Situs web utama fungsi adalah: http://www.di.ens.fr/~urban/function.html

Pengarang

 Caterina Urban, ETH Zurich, [email protected] 

Kontributor

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

Instalasi

Fungsi membutuhkan aplikasi dan pustaka berikut:

• Ocaml

   (sudo) apt-get install ocaml-interp
  

• Findlib

   (sudo) apt-get install ocaml-findlib
  

• Menhir: LR (1) Generator Parser

   (sudo) apt-get install menhir
  

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

   (sudo) apt-get install opam
  

• Dune: Ocaml Build System

   opam install dune
  

• Ounit

   opam install ounit
  

• Apron: Perpustakaan Domain Abstrak Numerik

   opam install apron
  

• Zarith: Operasi Integer Presisi Presisi Arbitrer

   opam install zarith
  

Fungsi kompilasi

Setelah semua pustaka yang diperlukan diinstal, fungsi dapat dikompilasi dengan 'Dune':

 dune build

Ini akan menghasilkan 'fungsi' program baris perintah di direktori proyek.

Atau, 'OcamlBuild' dapat digunakan untuk membangun fungsi dengan perintah berikut:

 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

Penggunaan

Penganalisa baris perintah dapat dipanggil menggunakan pola panggilan berikut:

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

di mana "file" adalah jalur ke file C yang akan dianalisis dan "analisis" jenis analisis yang akan dilakukan.

Penganalisa pertama-tama melakukan analisis jangkauan ke depan, dan kemudian analisis mundur untuk menemukan fungsi peringkat yang ditentukan oleh piecewise dan prasyarat yang cukup pada titik masuk untuk program untuk memenuhi properti yang dianalisis.

Opsi baris perintah umum berikut diakui (menunjukkan nilai default mereka):

 -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

Analisis menjawab benar jika berhasil membuktikan properti. Kalau tidak, jawabannya tidak diketahui.

Fungsi dapat menganalisis sifat -sifat berikut:

• Penghentian
• Jaminan / kambuh
• Computation-tree-Logic (CTL)

Penghentian

Untuk memeriksa penghentian, hubungi penganalisa dengan pola panggilan berikut:

 ./function <file> -termination [options]

Jaminan / kambuh

Pola panggilan berikut dapat digunakan untuk properti jaminan atau sifat kekambuhan:

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

di mana "properti_file" adalah jalur ke file yang berisi jaminan atau properti rekurensi.

CTL

Properti CTL dapat dianalisis menggunakan pola panggilan berikut:

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

di mana "properti" adalah properti CTL yang akan dianalisis.

Opsi baris perintah tambahan berikut ada untuk analisis CTL: (menunjukkan nilai default mereka):

 -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