Как использовать эту функцию Db.Slicing.Select.select_stmt с FRAMA-C

Question

Функция, которая в названии имеет следующую подпись:

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

Я хотел бы использовать эту функцию, но моя проблема заключается в аргумент set wich имеет тип 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 и довольно хорошо напечатать этот новый проект (конечно, вы можете также выполнять другие анализы).