SMAVE CODE ANALYZER
嵌入式C代碼分析與形式化驗證工具
SMAVE CODE ANALYZER
提供嵌入式C代碼分析與形式化驗證工具平臺/完成基于功能需求的C代碼分析與形式化驗證全流程工作
嵌入式C代碼分析與形式化驗證工具
SMAVE Code Analyzer 是一款專業(yè)嵌入式C代碼分析與形式化驗證工具，能基于MISRA-C編碼規(guī)范自動掃描代碼違規(guī)情況。為客戶在軟件開發(fā)過程中查找、識別、追蹤絕大部分的技術漏洞和邏輯漏洞，并在DevOps周期內(nèi)有效工作。它幫助開發(fā)團隊在早期檢測缺陷，從一開始就確保代碼安全、無憂、可靠。能夠完成基于功能需求的C代碼分析與形式化驗證全流程工作。
形式化驗證與規(guī)范語言
在軟件系統(tǒng)的開發(fā)過程中，如何檢查功能模塊是否符合設計預期并保證這些模塊能夠正確的組合在一起實現(xiàn)更復雜的功能，是一個核心問題。測試（testing）的方法在一定程度上能夠幫助我們發(fā)現(xiàn)一些問題；但要獲得更可靠的保證，往往需要借助程序驗證（verification）的方法：亦即使用某種形式化的語言（通常包括了對謂詞邏輯的支持）對程序行為作出規(guī)范，然后使用邏輯規(guī)則證明相關代碼符合給出的規(guī)范。
SMAVE Code Analyzer使用 C 語言的行為接口規(guī)范語言，它以特殊注釋的格式穿插在 C 代碼之中，精確嚴謹?shù)乜坍嬒嚓P代碼片段、乃至整個函數(shù)的行為和性質(zhì)。使用SMAVE Code Analyzer 的功能性驗證進行靜態(tài)分析能夠自動驗證其是否嚴格遵守了規(guī)范的約束。
_
為什么選擇SMAVE Code Analyzer
■ 良好的合規(guī)性
■ 安全，可靠的代碼
■ 更高的源碼質(zhì)量
■ 更快的發(fā)布
■ 簡單易用的操作界面
產(chǎn)品特點
支持DevOps
SMAVE Code Analyzer工具采用了持續(xù)集成與持續(xù)交付的設計理念，可以使得用戶的CI/CD流水線可以輕松包含靜態(tài)代碼分析功能。
■ 易于自動化: 提供命令行界面，可以以接口庫的方式提供相關的功能調(diào)用
■ 可擴展性: 基于OSGi規(guī)范，支持集成第三方插件或開發(fā)自己的插件
■ 開放性: 開放自定義擴展點和接口，方便用戶集成
簡單易用的UI操作界面
結(jié)構良好的用戶界面和可定制的窗口
基于需求的驗證
對需求規(guī)范進行管理，能夠基于用戶的每一條需求建立相應的驗證規(guī)則，從而通過對源碼的功能性驗證來測試需求的正確性
產(chǎn)品功能
需求規(guī)范管理
客戶可針對具體項目建立需求描述表格，并能夠?qū)⑿枨笈c功能驗證進行關聯(lián)，從而可以進行基于需求的功能驗證
編碼規(guī)范性檢查
根據(jù)MISRA C編碼標準自動檢測用戶的代碼識別安全關鍵系統(tǒng)中的潛在問題，并標記違反規(guī)則的代碼部分
功能性驗證
通過規(guī)范語言描述期望程序表現(xiàn)出的行為，自動驗證某段代碼是否滿足特定的性質(zhì)以及功能模塊的實現(xiàn)和調(diào)用是否合法
產(chǎn)品特點
缺陷檢查
■ 除零檢查
■ 左、右移越界檢查
■ 指針越界檢查
■ 浮點數(shù)轉(zhuǎn)整數(shù)檢查
■ 內(nèi)存訪問檢查
■ 局部變量和指針的初始化檢查
■ 常量表達式檢查
度量分析
能夠?qū)Τ绦蛑械囊恍┲笜藚?shù)進行度量分析，具體包括
■ 方法調(diào)用
■ 程序退出點
■ if語句
■ goto語句
■ 指針解引用
■ 聲明函數(shù)
■ 代碼行數(shù)
■ 圈復雜度
報告查看與生成
查看分析與驗證結(jié)果，并可以自定義模板生成分析與驗證報告