示例二：有符号数的溢出

下方是一个计算一季度总收入的函数，其中第12行对前三月销量进行了汇总，如果结果超过short的表示范围，则可能产生溢出。

类似示例一，我们可以对getMonthlySales函数进行插桩，并在W-AVC中验证。 通过验证，检查出以下溢出错误：

望安C代码自动验证平台W-AVC是由望安科技研发的C语⾔代码程序的形式化验证云平台。平台基于形式化验证技术，通过数学证明排查代码中的缺陷和安全隐患 ；同时通过开发验证⼈员编写的规约基准代码，⾃动检查代码中的安全漏洞，从而在开发流程的早期增强系统的安全性，减少现代⼤型软件架构带来的⻛险。

申请试用：

登陆w-avc.wonsec.com,申请免费试⽤。