Frama-C：在插件中添加注释

Question

我正在编写一个 Frama-C 插件。在这个插件中，我想为函数添加注释（例如，if function name = "test"，添加一个 requires 子句，说参数 == 1）。

我找到了函数Annotations.add_requires，但我不知道一些参数（Emitter.t、Identified_predicates）。字符串参数是谓词的函数名称还是自己的名称？

如何使用这个功能？谁能举个例子？

Answer 1

发射器识别您的插件并且必须声明它要修改的内容。在你的情况下，因为你想向规范添加属性，你可以构建它：

let emitter = Emitter.create "My plugin" [ Emitter.Funspec ]
    ~correctness:[] ~tuning:[]

现在，对于 kernel_function，这是一个如何构建第一个参数等于 1 的先决条件的示例：

let add_pre kf = match Kernel_function.get_formals kf with
  | [] -> ()
  | c_var::_ ->
    let l_var = Cil.cvar_to_lvar c_var in
    let var_term = Logic_const.tvar l_var in
    let cnst_term = Logic_const.tinteger 1 in
    let eq_pred = Logic_const.prel (Cil_types.Req, var_term, cnst_term) in
    let pred = Logic_const.new_predicate eq_pred in
    let bname = Cil.default_behavior_name in
    Annotations.add_requires emitter kf ~behavior:bname [pred]

Frama-C：在插件中添加注释

Frama-C: Add Annotation in Plugin

plugins

frama-c