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