联系我们+86 (021) 62118992sales@formal-tech.com        欢迎访问丰蕾科技官方网站   ACEPHERE & SMAVE




SMAVE CODE ANALYZER
嵌入式C代码分析与形式化验证工具

提供嵌入式C代码分析与形式化验证工具平台/完成基于功能需求的C代码分析与形式化验证全流程工作


嵌入式C代码分析与形式化验证工具 

SMAVE Code Analyzer 是一款专业嵌入式C代码分析与形式化验证工具,能基于MISRA-C编码规范自动扫描代码违规情况。为客户在软件开发过程中查找、识别、追踪绝大部分的技术漏洞和逻辑漏洞,并在DevOps周期内有效工作。它帮助开发团队在早期检测缺陷,从一开始就确保代码安全、无忧、可靠。能够完成基于功能需求的C代码分析与形式化验证全流程工作。


形式化验证与规范语言 

在软件系统的开发过程中,如何检查功能模块是否符合设计预期并保证这些模块能够正确的组合在一起实现更复杂的功能,是一个核心问题。测试(testing)的方法在一定程度上能够帮助我们发现一些问题;但要获得更可靠的保证,往往需要借助程序验证(verification)的方法:亦即使用某种形式化的语言(通常包括了对谓词逻辑的支持)对程序行为作出规范,然后使用逻辑规则证明相关代码符合给出的规范。

SMAVE Code Analyzer使用 C 语言的行为接口规范语言,它以特殊注释的格式穿插在 C 代码之中,精确严谨地刻画相关代码片段、乃至整个函数的行为和性质。使用SMAVE Code Analyzer 的功能性验证进行静态分析能够自动验证其是否严格遵守了规范的约束。

_

为什么选择SMAVE Code Analyzer  

■  良好的合规性

■  安全,可靠的代码

■  更高的源码质量

■  更快的发布

■  简单易用的操作界面


产品特点  

支持DevOps

SMAVE Code Analyzer工具采用了持续集成与持续交付的设计理念,可以使得用户的CI/CD流水线可以轻松包含静态代码分析功能。

 易于自动化:  提供命令行界面,可以以接口库的方式提供相关的功能调用

■  可扩展性:  基于OSGi规范,支持集成第三方插件或开发自己的插件

■  开放性:  开放自定义扩展点和接口,方便用户集成




简单易用的UI操作界面

结构良好的用户界面和可定制的窗口



 
基于需求的验证

对需求规范进行管理,能够基于用户的每一条需求建立相应的验证规则,从而通过对源码的功能性验证来测试需求的正确性

产品功能

需求规范管理


客户可针对具体项目建立需求描述表格,并能够将需求与功能验证进行关联,从而可以进行基于需求的功能验证

  

编码规范性检查


根据MISRA C编码标准自动检测用户的代码识别安全关键系统中的潜在问题,并标记违反规则的代码部分

 

功能性验证


通过规范语言描述期望程序表现出的行为,自动验证某段代码是否满足特定的性质以及功能模块的实现和调用是否合法

产品特点   

缺陷检查



■  除零检查

■  左、右移越界检查

■  指针越界检查

■  浮点数转整数检查

■  内存访问检查

■  局部变量和指针的初始化检查

■  常量表达式检查






   

 度量分析


能够对程序中的一些指标参数进行度量分析,具体包括

■  方法调用      

■  程序退出点

■  if语句

■  goto语句

■  指针解引用

■  声明函数

■  代码行数

■  圈复杂度

  

报告查看与生成


查看分析与验证结果,并可以自定义模板生成分析与验证报告