smackers/smackسلسلة أدوات تحقق برمجية معيارية تترجم LLVM IR إلى لغة التحقق الوسيطة Boogie للتحقق من التوكيدات المقيدة والتجريبية غير المقيدة في برامج C.
SMACK هو سلسلة أدوات تحقق برمجي معيارية ومدقق برمجي مستقل. يمكن استخدامه للتحقق من التأكيدات في برامج الإدخال. في الوضع الافتراضي، يتم التحقق من التأكيدات حتى حد معين لتكرار الحلقات وعمق التكرار؛ كما يحتوي على دعم تجريبي للتحقق غير المحدود أيضًا. يتعامل SMACK مع الميزات المعقدة للغة C، بما في ذلك تخصيص الذاكرة الديناميكي، الحساب على المؤشرات، والعمليات على البتات.
تحت الغطاء، SMACK هو مُترجم من التمثيل الوسيط الشائع (IR) لمُحَوِّل LLVM إلى لغة التحقق الوسيطة (IVL) Boogie. الاستفادة من LLVM IR تستغل العدد المتزايد من الواجهات الأمامية للمُحَوِّلات، التحسينات، والتحليلات. حاليًا، يدعم SMACK لغة C فقط عبر مُحَوِّل Clang، رغم أننا نعمل على تقديم دعم للغات إضافية. استهداف Boogie يستفيد من منصة قانونية تبسط تنفيذ خوارزميات التحقق، فحص النماذج، والتفسير التجريدي. حاليًا، يستفيد SMACK من المُدقِّقين Boogie و Corral.
انظر أدناه لمتطلبات النظام، التثبيت، الاستخدام، وكل شيء آخر.
نحن مهتمون جدًا بتجربتك مع SMACK. يُرجى التواصل مع Zvonimir أو Michael أو Shaobo لأي ملاحظات.
للأسئلة العامة، استشر أولاً الأسئلة الشائعة.
إذا كان هناك شيء معطل أو مفقود، افتح مشكلة.
كملاذ أخير، أرسل بريدًا إلكترونيًا إلى Michael و Zvonimir و Shaobo.
للبقاء على اطلاع بالتحديثات، يمكنك متابعة صفحة SMACK على Github.
تم دعم مشروع SMACK جزئيًا من قبل المؤسسة الوطنية للعلوم (NSF)، VMware، Amazon، و Microsoft Research. كما نعتمد على بنية Emulab بجامعة يوتا للاختبار المكثف لـ SMACK.
