3
软件验证工具链
source link: https://www.oschina.net/p/smack
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
SMACK首页、文档和下载 - 软件验证工具链 - OSCHINA - 中文开源技术交流社区
SMACK即是一个模块化的软件验证工具链，又是一个独立的软件验证工具。它可以被用于验证输入程序里的断言。默认模式下SMACK对断言的验证是有对循环/递归的上限。同时，SMACK实现了对无上限的验证的初步支持。SMACK可以处理复杂的C语言特性，如动态内存分配，指针操作，和位运算。
本质上SMACK是一个从LLVM中间语言(IR)到Boogie中间语言的翻译器。使用LLVM IR使得SMACK可以利用大量的支持LLVM IR的编译器，对LLVM IR的优化和分析。目前，SMACK通过Clang编译器实现对C语言的支持。同时，我们也在开发对其他语言的支持。使用Boogie使得SMACK可以利用一个通用的验证平台，该平台简化了对验证方法的实现。目前，SMACK支持Boogie和Corral两个后端验证工具。
对SMACK的安装请参照该文档：https://github.com/smackers/smack/blob/main/docs/installation.md
对SMACK的使用请参照该文档：https://github.com/smackers/smack/blob/main/docs/running.md
展开阅读全文
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK