如何使用此功能Db.Slicing.Select.select_stmt與郵資-C

Question

這是標題中的函數具有以下特徵：

val select_stmt : 
(set -> spare:bool -> Cil_types.stmt -> Cil_types.kernel_function -> set) 
    Pervasives.ref 

我想使用這個功能，但我的問題是關於參數set至少有一個類型type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t。我不知道如何初始化這個參數，然後我想打印結果。如果有人能給我一個例子

Answer 1

只是在select_stmt之上，你的值爲empty_selects，其文檔表明它代表一個空選擇。在此之後，切片的API是有點神祕，但如果我沒有記錯的話，你應該能夠獲得一個切片具有大致如下（未測試）的東西：

let prj = 
Db.Slicing.(
    let sp = !Project.mk_project "my slicing project" in 
    let selection = Select.(!select_stmt empty_selects s kf) in 
    let() = Request.add_selection sp selection in 
    Project.extract "my frama-c project" sp) 
in 
File.pretty_ast ~prj() 

基本上，你必須創建一個切片項目，您可以在其中設置一定數量的選項，特別包括所需的切片標準。當您對切片項目的狀態感到滿意時，可以從中提取新的Frama-C項目，並正常打印此新項目（當然，您也可以對其進行其他分析）。