intAbs

ReadMe

يدور هذا المستودع حول التفسير التجريدي المعياري للخيط (باستخدام مكتبة المئزر) للبرامج التي تعتمد على المقاطعة من خلال اعتماد معلومات الأولوية.

الكود المصدر هو إصدار معدّل من https://github.com/markus-kusano/watts

في الوقت الحالي ، لا يتم تنظيف جميع الملفات بما في ذلك ملفات الاختبار.

ومع ذلك ، يمكن طباعة مجموعة فرعية من جداول النتائج حيث يتم تحميل بعض ملفات الإخراج.

نقلا عن Intabs

 @inproceedings{DBLP:conf/kbse/SungKW17,
  author    = {Chungha Sung and
               Markus Kusano and
               Chao Wang},
  title     = {Modular verification of interrupt-driven software},
  booktitle = {Proceedings of the 32nd {IEEE/ACM} International Conference on Automated
               Software Engineering, {ASE} 2017, Urbana, IL, USA, October 30 - November
               03, 2017},
  pages     = {206--216},
  year      = {2017},
  crossref  = {DBLP:conf/kbse/2017},
  url       = {https://doi.org/10.1109/ASE.2017.8115634},
  doi       = {10.1109/ASE.2017.8115634},
  timestamp = {Fri, 01 Dec 2017 22:44:10 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/kbse/SungKW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

مبنى

البرنامج هو تمريرة LLVM OPT. تم تصميمه باستخدام Cmake. نظرًا لأننا نستخدم Cmake ، فمن المحتمل أن يتطلب ذلك الإصدار LLVM 3.6.0

قم بتعديل متغير ملف cmakelists Apron_Prefix ليكون الموقع الذي يتم تثبيت المئزر

على افتراض أن ملفات مكتبة LLVM في موقع قياسي (المزيد على هذا أدناه) ، ببساطة:

 mkdir build
cd build
cmake ../
make

نتيجة عملية الإنشاء هي ملف. لذا ، libworklistai.so

إذا كنت بحاجة إلى إخبار Cmake بمكان LLVM ، فأنت بحاجة إلى إضافة الخيار -dllvm_dir ، على سبيل المثال ،

cmake -dllvm_dir =/home/chungha/src/share/llvm/cmake ../

يجب أن يكون الدليل الذي تم تمريره إلى LLVM_DIR هو الموقع الذي تكون فيه ملفات LLVM CMAKE (على سبيل المثال ، LLVM-CONFIG.CMAKE).

قد تحتاج أيضًا إلى تعيين -DZ3_INC و -DZ3_LIB إلى دليل تضمين ، وملف المكتبة لـ Z3 ، على التوالي.

مسار الاختبار

تحتاج إلى تعديل مسار LLVM ومسار البناء في ملف SRC/Test/Export.sh لاختبار البرنامج مثل LLVM_PREFIX ، WorkList_SO ، Z3_BIN.

تأكيد الاستخدام

إذا كنت ترغب في التحقق من ثبات البرنامج باستخدام Assert ، فيجب عليك استخدامها بهذه الطريقة.

بدلاً من استخدام assert(a==1) ، عليك أن تكتب if (a != 1) { assert(0); } .

نظرًا لعلاقة ما بعد السيطرة ، أحتاج إلى تنفيذ أداتي لدعم هذه الحالة فقط (Assert يجعل البرنامج غير قابل للوصول حتى يتم فقد بعض علاقة ما بعد السيطرة).

وصف الدليل

• ICBMC: هذا هو الدليل الذي اختبرت فيه ملف ICBMC الثنائي من ورقة Date15 مع معاييري.

• SRC: يحتوي على التنفيذ الرئيسي (Worlist-AI ، utils ، cmakelists.txt) ودليل اختبار (اختبار)

• SRC/Test: يحتوي على ملفات نصية لتشغيل البرامج الاختبار والمعيار. أيضا ، يتم تضمين ملفات النتائج في كل دليل.