如何使用此功能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项目，并正常打印此新项目（当然，您也可以对其进行其他分析）。