3

我正在学习如何开发 Frama-C 插件。在阅读了 Frama-C 开发人员手册并完成了 CFG 插件示例之后，我尝试编写一个基本脚本来打印 C 文件中的所有注释。我想出了这个：

open Cil_types

class print_annot out = object
    inherit Visitor.frama_c_inplace

method vstmt_aux s =
let annots = Annotations.code_annot s in
let anleng = List.length annots in
if anleng <= 0 then Format.fprintf out "Empty List\n"
  else
  Format.fprintf out "Number of Annotations: %d\n" anleng;
  List.iter (fun annot -> Format.fprintf out " -> s%d\n" annot.annot_id) annots;
  Cil.DoChildren
end

let run () =
let chan = open_out "annots.out" in
let fmt = Format.formatter_of_out_channel chan in
Visitor.visitFramacFileSameGlobals (new print_annot fmt) (Ast.get());
close_out chan

let () = Db.Main.extend run

即使输入文件具有 ACSL 注释并且从不打印注释 ID，它也总是说列表为空。我究竟做错了什么？

编辑：

带有以下代码的示例：

 /*@ requires y >= 0;
 @ ensures \result >= 0;
 */

 int g(int y){
int x=0;

if(y>0){
    x=100;
    x=x+50;
    x=x-100;
}else{
    x = x - 150;
    x=x-100;
    x=x+100;
}
return x;
    }

    void main(){
int a = g(0);

 }

并使用以下命令调用 frama-c：

 $ frama-c -load-script annot_script.ml condi.c

给出以下输出：

 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
4

1 回答 1

3

在您的示例中，没有任何注释附加到语句中。therequires和 theensures是函数契约的一部分，并附加到函数g，而不是g.

例如，将附加到语句的注释将/*@ assert x == 150; */位于 line 之后x=x+50;。

如果我修改condi.c以插入此断言，那么使用相同的命令行，我得到：

空列表
空列表
空列表
空列表
注释数量：1
 -> s1
空列表
空列表
空列表
空列表
空列表
空列表
空列表

您的脚本似乎按预期工作，“预期”值对应于打印附加到语句的注释。

于 2014-05-07T19:39:12.707 回答