我实际上正在编写一个包含这四个文件的个人 Frama-C 插件:
分析TU_core.ml
module Options = AnalyseTU_options
open Cil_types
let rec member x list1 = match list1 with
[]->false
|hd :: tl -> if hd = x then true else member x tl
let rec sandr list2 result= match list2 with
[]-> Format.fprintf out "job termine"
|hd :: tl -> if member hd result = false then begin result::hd ; Format.fprintf out hd; sandr tl result end
else sandr tl result
class print_analyse out = object
inherit Visitor.frama_c_inplace
method vstmt s=
let listing =[] in
let impacted = !Db.Impact.compute_pragmas in
let impacted2= impacted.Stmt.loc in
sandr impacted2 listing;
Cil.DoChildren
end
和 :
分析TU_register.ml
open AnalyseTU_options
open AnalyseTU_core
let run () =
if Enabled.get () then
let filename=OutputFile.get () in
let chan = open_out filename in
let fmt = Format.formatter_of_out_channel chan in
Visitor.visitFramacFileSameGlobals (new print_analyse fmt) (Ast.get ());
close_out chan
let () = Db.Main.extend run
和 :
分析TU_options.ml
module Self = Plugin.register
(struct
let name = "analyse TU"
let shortname = "TU"
let help = "impacted statements computation from a source code modification and display consequently unit tests to be run in an output file"
end)
module Enabled = Self.False
(struct
let optilon_name = "-TU"
let help = "when on (off by default), give the unit tests to be run"
end)
module OutputFile = Self.String
(struct
let option_name = "-TU-output"
let default = "TUresults.txt"
let arg_name = "output-file"
let help = "name of the output file"
end)
最后是makefile:
FRAMAC_SHARE := $(shell frama-c -print-path)
FRAMAC_LIBDIR := $(shell frama-c -print-libpath)
PLUGIN_NAME = analyseTU
PLUGIN_CMO = analyseTU_options analyseTU_core analyseTU_register
include $(FRAMAC_SHARE)/Makefile.dynamic
所以,当我用 make 命令编译它时,我实际上得到了:
FILE "analyseTU_core.ml", line 9 :
Error: unbound value out
make : *** [analyseTU_core.cmo] erreur 2
我当时认为这是因为编译器不知道“out”这一事实,因此我将“out”替换为“chan”。顺便说一句,我遇到了同样的错误。
开发人员指南教程的代码中未定义“out”这一事实最终让我认为这个错误不是我想的那样......
你有没有遇到过?如果是,您是如何处理的?