[發明專利]一種航天嵌入式C語言軟件運行時錯誤的靜態分析方法

有效

• 申請號: 201110291315.2
• 申請日: 2011-09-29
• 公開（公告）號: CN102508766A
• 公開（公告）日: 2012-06-20
• 發明（設計）人: 王崑聲;詹海潭;經小川;張剛;李寧
• 申請（專利權）人: 中國航天科技集團公司第七一〇研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 中國航天科技專利中心 11009
• 代理人: 臧春喜

1.一種航天嵌入式C語言軟件運行時錯誤的靜態分析方法，其特征在于包括以下步驟：

(1)對航天嵌入式C語言軟件運行時錯誤進行分類，按照分類后每類錯誤的屬性模式構造屬性狀態機，所述屬性狀態機包括程序運行過程中可能出現的屬性狀態D_i，i＝{1，…n}，n為每類錯誤中的屬性狀態總數，D_i包括程序運行過程中可能的出現的錯誤狀態；

(2)按照程序的控制流程圖和運行時錯誤的屬性狀態機，根據控制流程圖中位置l處的節點信息和輸入屬性狀態σ_{l_in}，獲得經位置l處的節點處理后的輸出屬性狀態σ_{l_out}和路徑條件C_s，l，其中，s為到達位置l處的路徑；

(3)判斷σ_{l_out}與屬性狀態D_i的關系：

若σ_{l_out}為D_i中的錯誤狀態，則將路徑條件C_s，l作為可能出現的錯誤提示輸出，并不再對C_s，l進行后續分析；否則，將σ_{l_out}作為下一個位置處的輸入屬性狀態返回步驟(2)，直到程序出口。

2.根據權利要求1所述的一種航天嵌入式C語言軟件運行時錯誤的靜態分析方法，其特征在于：所述屬性狀態機由狀態轉移集合T組成，所述狀態轉移集合T為D_i×conditions_i→D_k，i，k＝{1，…n}，其中，D_i和D_k為屬性狀態，D_k為源屬性狀態D_i在轉移條件為conditions_i時的目標屬性狀態；所述轉移條件conditions_i為根據C語言確定的對數據流的操作。

3.根據權利要求1所述的一種航天嵌入式C語言軟件運行時錯誤的靜態分析方法，其特征在于：在所述步驟(2)中，對控制流程圖中位置l_j處的節點信息進行判斷：

若位置l處的節點為匯合節點，則將相同的輸入屬性狀態σ_{l_in}的路徑條件進行合并，然后獲得經位置l處的節點處理后的輸出屬性狀態σ_{l_out}和合并后的輸出路徑條件C_s，l；

若位置l處的節點為分支節點，比較路徑條件C_s，l中的變量取值與當前判斷謂詞取值的交集，若交集為空，表示該位置的輸入屬性狀態σ_{l_in}的路徑條件C_s，l和當前分支組合后為不可達路徑，則不記錄不可達路徑上的屬性數據流信息。

4.根據權利要求1所述的一種航天嵌入式C語言軟件運行時錯誤的靜態分析方法，其特征在于：所述屬性狀態機根據錯誤的屬性模式可分為：空指針解引用屬性狀態機、資源泄露屬性狀態機、未初始化變量引用屬性狀態機和除零錯誤屬性狀態機。