×

SMACK软件验证工具链

消耗积分:0 | 格式:zip | 大小:1.03 MB | 2022-06-16

英雄孤寂

分享资料个

授权协议 MIT
开发语言 C/C++ Python
操作系统 跨平台
软件类型 开源软件
所属分类 开发工具、 代码管理分析/审查/优化

软件简介

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已经用于百度开源项目SGXRay。

对SMACK的安装请参照该文档

对SMACK的使用请参照该文档

对SMACK的使用问题请联系何少博(shaobohe@baidu.com)

 

下载并关注上传者 低至0.43元/天 开通VIP 免费下载

声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉

评论(0)
发评论

下载排行榜

全部0条评论

快来发表一下你的评论吧 !