jayhorn
version 0.7
| يتقن | ||||
|---|---|---|---|---|
| التطور |
جافا وقرن الجمل
Jayhorn هي أداة فحص نموذج البرمجيات لجافا. يحاول Jayhorn العثور على دليل على أن بعض الدول السيئة في برنامج Java لا يمكن الوصول إليها أبدًا. يتم تحديد هذه الحالات السيئة عن طريق إضافة تأكيدات وقت التشغيل (حيث قد يتم إنشاء بعض التأكيدات ، على سبيل المثال ، أنه يجب ألا يكون مرجع الكائن فارغًا قبل الوصول إليه).
يحاول Jayhorn أن يخطئ إلى جانب الدقة ، عندما لا يكون قادرًا على إثبات أن التأكيد دائمًا ، سيزعم أن التأكيد قد ينتهك (يسمى هذا السلامة). Jayhorn هو حاليًا (Modulo Bugs) لـ Java الذي يستخدم مؤشر ترابط واحد ، وليس لديه تحميل فئة ديناميكية ، ولا يقومون بعمليات معقدة في المهيئات الثابتة.
للحصول على معلومات حول كيفية تنزيل وتشغيل Jayhorn تحقق من موقعنا على الويب. للحصول على معلومات حول كيفية تنفيذ Jayhorn ، تحقق من مدونة Jayhorn Development.
انضم إلى الدردشة
./gradlew assemble
java -jar jayhorn/build/libs/jayhorn.jar -help
java -jar jayhorn/build/libs/jayhorn.jar -j example/classes -solution -traceوقد تم هذا المشروع بروح السعادة. عند بناء تحليلات البرنامج العملي ، غالبًا ما يكون من الضروري قطع الزوايا. من أجل أن نكون منفتحين على ميزات اللغة التي لا ندعمها أو ندعمها جزئيًا فقط ، فإننا نرفق بيان السعة هذا.
لا يحتوي تحليلنا على معالجة صوتية بالكامل للميزات التالية:
تم إنتاج هذا البيان مع مولد بيان السعادة من Soundiness.org.
Jayhorn مفتوح المصدر وتوزيعه بموجب ترخيص معهد ماساتشوستس للتكنولوجيا.
تشمل المكتبات المستخدمة في Jayhorn ، على وجه الخصوص:
تم تمويل Jayhorn جزئيًا:
أي آراء أو النتائج والاستنتاجات أو التوصيات المعبر عنها في هذه المادة هي آراء المؤلفين (المؤلفين) لا تعكس بالضرورة آراء AFRL أو DARPA أو NSF أو مجلس الأبحاث السويدي.
