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