Frama-C: Add Annotation in Plugin

Question

I am writing a Frama-C-plugin. In this plugin, I want to add annotations to functions (e.g. if function name = "test", add a requires clause, saying parameter == 1).

I found the function Annotations.add_requires, but I don't know some of the parameters (Emitter.t, Identified_predicates). Is the string-parameter the function name or an own name for the predicate?

How do I use this function? Can anyone show an example?

Answer 1

The emitter identify your plugin and has to declare what it is suppose to modify. In your case, as you want to add properties to the specifications, you can build it with:

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

Now, for a kernel_function this is an example of how to build a precondition saying that the first parameter is equal to one:

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]