SMACK 正在参加 2021 年度 OSC 中国开源项目评选,请投票支持!
SMACK 在 2021 年度 OSC 中国开源项目评选 中已获得 {{ projectVoteCount }} 票,请投票支持!
2021 年度 OSC 中国开源项目评选 正在火热进行中,快来投票支持你喜欢的开源项目!
2021 年度 OSC 中国开源项目评选 >>> 中场回顾
SMACK 获得 2021 年度 OSC 中国开源项目评选「最佳人气项目」 !
授权协议 MIT
开发语言 C/C++ Python
操作系统 跨平台
软件类型 开源软件
开源组织
地区 不详
投 递 者 何少博
适用人群 未知
收录时间 2022-02-24

软件简介

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)

展开阅读全文

代码

的 Gitee 指数为
超过 的项目

评论

点击引领话题📣
暂无内容
发表了博客
{{o.pubDate | formatDate}}

{{formatAllHtml(o.title)}}

{{parseInt(o.replyCount) | bigNumberTransform}}
{{parseInt(o.viewCount) | bigNumberTransform}}
没有更多内容
暂无内容
发表了问答
{{o.pubDate | formatDate}}

{{formatAllHtml(o.title)}}

{{parseInt(o.replyCount) | bigNumberTransform}}
{{parseInt(o.viewCount) | bigNumberTransform}}
没有更多内容
暂无内容
0 评论
4 收藏
分享
OSCHINA
登录后可查看更多优质内容
返回顶部
顶部
返回顶部
顶部