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

【问题标题】：Frama-C: Add Annotation in PluginFrama-C：在插件中添加注释
【发布时间】：2016-03-31 15:57:12
【问题描述】：

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

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

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

【问题讨论】：

你尝试了吗？您是否设法找到“测试”函数（kernel_function）及其“参数”的变量（varinfo）？现在，在使用add_requires 之前，您必须构建谓词parameter == 1，对吗？你知道怎么做吗？
我得到了 kernel_function 和 varinfo。我将第三个参数（我认为是名称）设置为“test”。现在还有 2 个参数（第一个和最后一个）我不知道如何构建它们。 Emitter 有一个创建函数，但它有几个列表，我不知道它们在哪里（我现在尝试了Emitter.create "name" [Code_annot] [] []。此外，我不知道如何构建谓词列表，因为它包含其他一些奇怪的东西（所以我也无法使用名称和发射器测试其他两次尝试）。
我现在尝试了这个：let pred = Cil_types.Ptrue in let id_pred = {ip_name = [];ip_loc= location; ip_id= 1; ip_content= pred}，但我不知道应该使用什么位置？

标签： plugins frama-c

【解决方案1】：

发射器识别您的插件并且必须声明它应该修改的内容。在您的情况下，当您想向规范添加属性时，您可以使用以下方式构建它：

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

现在，对于kernel_function，这是一个示例，说明如何构建一个前提条件，即第一个参数等于一个：

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]

【讨论】：

我正在使用您的代码 sn-p（这似乎是有道理的）。以下问题：当我写 //@requires config == 1;在 C 代码中并将 add_pre 调用到注释中，值分析显示config_0 -> {{ NULL -> {1} }}，但是当删除手写的要求并调用您的函数时，它最终为config_0 -> {{ NULL -> [--..--] }}（就像它没有做任何事情）在这两种情况下，我在调用您的函数后调用!Db.Value.compute ()（在成功的情况下已注释）它不应该以同样的方式反应吗？
也许可以尝试使用-print 选项来查看是否正确添加了属性。
也可以试试frama-c file.c -your-plugin-option -then -val（这个似乎在这里工作）。
也许Value 在调用add_pre 之前已经计算好了，在这种情况下，你对!Db.Value.compute () 的调用可能什么都不做。
谢谢，您的意见解决了我的问题。我的部分代码有一个小错误 :) 一个问题：你在哪里学习了如何使用该框架？是否有任何好的教程，或者是否有可用的示例代码？开发者指南只展示了一小部分，如果没有 Stackoverflow 的帮助，完成这段代码需要几个世纪的时间