当前位置:统一通信/协作企业动态 → 正文

Facebook开源了静态分析工具Infer

责任编辑:editor006 作者:Abel Avram |来源:企业网D1Net  2015-06-22 20:53:07 本文摘自:INFOQ

Facebook开源了适用于分析C、Java和Objective-C代码的静态分析工具Infer。

Infer是Facebook的开发团队在代码提交内部评审时,用来执行增量分析的一款静态分析工具,在代码提交到代码库或者部署到用户的设备之前找出bug。由OCaml语言编写的Infer目前能检测出空指针访问、资源泄露以及内存泄露,可对C、Java或Objective-C代码进行检测。Facebook使用Infer自动验证iOS和安卓上的移动应用的代码,bug报告的正确率达80%。

Infer通过捕获编译命令,把要被编译的文件转换为可用于分析潜在错误的中间语言格式。整个过程是增量进行的,意味着通常只有那些有修改过并提交编译的文件才会被Infer分析。Infer还集成了大量的构建或编译工具,包括Gradle、Maven、Buck、Xcodebuild、clang、make和javac。

有一些类型的错误能用Infer检测出,关于它们的更多细节内容可见此页。Infer未来有望能加强对数组越界错误、转换异常和污染数据泄露的检测,Facebook目前已开始着手开发这些功能,但暂不可用。

在被问及能否增强Infer的功能,以使其可找出其他错误,并能应用于其他语言编写的代码时,Facebook的发言人答复InfoQ:“我们认为,关于Infer,这才只是一个开始,公司未来将持续致力于释放更多的价值给程序员”,并表示Facebook希望能与社区一起合作,来进一步完善Infer:

Infer做的不错,不过仍有许多跨工程组织的开放问题有待解决。一旦Facebook开源了Infer,就可以同许多工程组织、研究组织和学术组织进行合作,通过社区的努力,有可能最终Infer会增加一些新特性,能用来发现新类型的bug,甚至可以应用到新的语言上。

据Facebook透露,Infer根植于两大基本理论之上,其一是霍尔逻辑,一种用于推理计算机程序正确性的形式系统,另一个是抽象解释,该理论用于测度程序语义的逼近结果,此外还涉及其它一些研究成果,例如Separation Logic和Bi-abduction。

Infer的源代码可在GitHub上获取。

关键字:InferFacebookGitHub

本文摘自:INFOQ

x Facebook开源了静态分析工具Infer 扫一扫
分享本文到朋友圈
当前位置:统一通信/协作企业动态 → 正文

Facebook开源了静态分析工具Infer

责任编辑:editor006 作者:Abel Avram |来源:企业网D1Net  2015-06-22 20:53:07 本文摘自:INFOQ

Facebook开源了适用于分析C、Java和Objective-C代码的静态分析工具Infer。

Infer是Facebook的开发团队在代码提交内部评审时,用来执行增量分析的一款静态分析工具,在代码提交到代码库或者部署到用户的设备之前找出bug。由OCaml语言编写的Infer目前能检测出空指针访问、资源泄露以及内存泄露,可对C、Java或Objective-C代码进行检测。Facebook使用Infer自动验证iOS和安卓上的移动应用的代码,bug报告的正确率达80%。

Infer通过捕获编译命令,把要被编译的文件转换为可用于分析潜在错误的中间语言格式。整个过程是增量进行的,意味着通常只有那些有修改过并提交编译的文件才会被Infer分析。Infer还集成了大量的构建或编译工具,包括Gradle、Maven、Buck、Xcodebuild、clang、make和javac。

有一些类型的错误能用Infer检测出,关于它们的更多细节内容可见此页。Infer未来有望能加强对数组越界错误、转换异常和污染数据泄露的检测,Facebook目前已开始着手开发这些功能,但暂不可用。

在被问及能否增强Infer的功能,以使其可找出其他错误,并能应用于其他语言编写的代码时,Facebook的发言人答复InfoQ:“我们认为,关于Infer,这才只是一个开始,公司未来将持续致力于释放更多的价值给程序员”,并表示Facebook希望能与社区一起合作,来进一步完善Infer:

Infer做的不错,不过仍有许多跨工程组织的开放问题有待解决。一旦Facebook开源了Infer,就可以同许多工程组织、研究组织和学术组织进行合作,通过社区的努力,有可能最终Infer会增加一些新特性,能用来发现新类型的bug,甚至可以应用到新的语言上。

据Facebook透露,Infer根植于两大基本理论之上,其一是霍尔逻辑,一种用于推理计算机程序正确性的形式系统,另一个是抽象解释,该理论用于测度程序语义的逼近结果,此外还涉及其它一些研究成果,例如Separation Logic和Bi-abduction。

Infer的源代码可在GitHub上获取。

关键字:InferFacebookGitHub

本文摘自:INFOQ

电子周刊
回到顶部

关于我们联系我们版权声明隐私条款广告服务友情链接投稿中心招贤纳士

企业网版权所有 ©2010-2024 京ICP备09108050号-6 京公网安备 11010502049343号

^