المنتصر - عبر الإنترنت في السحابة

برنامج:

اسم

المنتصر - يحاول تنفيذ شروط التحقق باستخدام أدوات حل SMT

موجز

منتصر [وحدة]

الوصف

إنّ كافة أنواع عهود الـ منتصر الأمر عبارة عن غلاف حول ViCToR (VCT) مما يبسط استخدامه. فيكتور
يترجم شروط التحقق من SPARK إلى SMTlib ويغذيها إلى محلل SMT.
يأتي SPARK مزودًا بأحد حلول SMT، بديل ergo، ولكن من الممكن استخدام أدوات حل أخرى
مثل cvc3.

الغرض من استخدام المنتصر هو تفريغ رأس المال الاستثماري الحقيقي الذي خلفه المبسط وليس
استبدال المبسط. يرجى أيضًا ملاحظة أن ViCToR يعتبر تجريبيًا
ميزة في الوقت الراهن.

تلخص صفحة الدليل هذه فقط ملف منتصر أعلام سطر الأوامر، يرجى الرجوع إلى كامل
دليل VictorWrapper لمزيد من المعلومات.

OPTIONS

هذه الخيارات لا تتبع تمامًا صيغة سطر أوامر جنو حيث تبدأ الخيارات بها
شرطة واحدة بدلاً من الاثنين المعتاد.

-h, -مساعدة
يظهر تعليمات سطر الأوامر.

-t =SECONDS
انتهت مهلة حل SMT بعد هذه الثواني العديدة (افتراضيًا 5) باستخدام ulimit. إلى
تعطيل المهلة حدد 0.

م =ميغابايت
قم بقصر حل SMT على هذا العدد من MiB من الذاكرة الافتراضية (بشكل افتراضي لا يوجد حد) باستخدام
ulimit.

-v تجاهل وجود أي ملفات siv وقم بمعالجة ملفات vcg فقط. افتراضيا، نظرا
a UNIT مثل foo، سيحاول المنتصر أولاً معالجة foo.siv ثم يتراجع
إلى foo.vcg.

-عادي الوضع العادي — قمع التوقيتات والإصدارات.

-حلالا=محلول
يحدد حلاً بديلاً لـ SMT. بشكل افتراضي نستخدم alt-ergo. يمكن أن يكون واحدا من البديل
إرجو، cvc3، yices أو z3. يتم توزيع حل Alt-ergo باستخدام SPARK. سي في سي 3
الحل جزء من دبيان. تعد أدوات حل yices وz3 ملكية خاصة.

استخدم المنتصر عبر الإنترنت باستخدام خدمات onworks.net