الصفحة الرئيسية>كود المصدر JSP>فئات أخرى
تنزيل

وظيفة

الوظيفة هي محلل ثابت للبحثية مصمم لإثبات الإنهاء الشرطي والضمان الشرطي وخصائص التكرار لبرامج 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/~urpan/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

  • مينهر: LR (1) مولد محلل 

     (sudo) apt-get install menhir

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

     (sudo) apt-get install opam

  • الكثبان الرملية: نظام بناء 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

يجيب المحلل صحيحًا في حال كان بإمكانه إثبات العقار بنجاح. خلاف ذلك ، يجيب غير معروف.

يمكن للوظيفة تحليل الخصائص التالية:

  • إنهاء
  • ضمان / تكرار
  • الحساب-شجرة السودوك (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]

حيث "Property" هي خاصية 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
يوسع
معلومات إضافية
تطبيقات ذات صلة
نوصي لك
أخبار ذات صلة الكل