Frama-C插件测试报错：logic variable未声明的原因与解决

我实现了《Developer Manual》4.17.7章节的示例代码，这是一个复制访问者插件，可为程序中每个除法操作添加除数非零的断言。直接将插件应用于含除法的C源码时可得到预期注解，但使用带-sandbox参数的测试代码运行时，触发AST完整性检查错误，提示“logic variable b (25) is not declared”，导致Frama-C异常终止。

插件代码 #

open Cil_types
open Cil
module M = Plugin.Register

let syntax_alarm =
  Emitter.create "Syntactic check" [ Emitter.Code_annot ] ~correctness:[]
    ~tuning:[]

class non_zero_divisor prj =
  object (self)
    inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)

    method! vexpr e =
      match e.enode with
      | BinOp ((Div | Mod), _, denom, _) ->
          let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
          let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
          let stmt =
            match self#current_kinstr with
            | Kglobal -> assert false
            | Kstmt s -> s
          in
          let kf = Option.get self#current_kf in
          let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
          Options.Self.result "NewStmt: %a" Printer.pp_stmt new_stmt;
          let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
          Queue.add
            (fun () ->
              Annotations.add_assert syntax_alarm ~kf:new_kf new_stmt assertion)
            self#get_filling_actions;
          DoChildren
      | _ -> DoChildren
  end

let execute () =
  ignore
    (File.create_project_from_visitor "syntactic check" (new non_zero_divisor))

测试代码 #

/* run.config
OPT: -autoload-plugins -sandbox
*/

void main() {
    int a, b, c;
    a = 4;
    b = 2;
    c = a/b;
}

错误输出 #

...
[kernel] tests/s1/test.c:9: Failure: 
  [AST Integrity Check]
  AST of syntactic check
  logic variable b (25) is not declared
[kernel] Current source was: tests/s1/test.c:5
  The full backtrace is:
  Raised at Project.on in file "src/libraries/project/project.ml", line 405, characters 59-66
  Called from File.init_project_from_visitor in file "src/kernel_services/ast_queries/file.ml", line 1818, characters 4-64
  Called from File.create_project_from_visitor in file "src/kernel_services/ast_queries/file.ml", line 1842, characters 2-43
  Called from Sandbox_visitor.execute in file "sandbox_visitor.ml", line 37, characters 4-79
  Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
  Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
  Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
  Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
  Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
  
  Frama-C aborted: internal error.
  Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
  Your Frama-C version is 24.0 (Chromium).
  Note that a version and a backtrace alone often do not contain enough
  information to understand the bug. Guidelines for reporting bugs are at:
  https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs

使用-sandbox参数时，Frama-C会创建独立的项目副本，所有AST节点（变量、语句、函数等）都会被复制到新项目中。原代码直接使用原项目的denom表达式转换为逻辑项，再将这个逻辑项添加到新项目的断言里——但原项目的变量b并未注册到新项目的逻辑环境中，导致AST完整性检查时判定变量未声明。

核心问题是：跨项目引用AST节点，违反了Frama-C的项目隔离机制。

必须确保断言中使用的逻辑项基于新项目中的节点创建。具体来说，不能直接使用原项目的denom表达式，需先通过Visitor_behavior.Get.expr获取该表达式在新项目中的副本，再用副本转换为逻辑项并构建断言。

修改后的插件代码 #

open Cil_types
open Cil
module M = Plugin.Register

let syntax_alarm =
  Emitter.create "Syntactic check" [ Emitter.Code_annot ] ~correctness:[]
    ~tuning:[]

class non_zero_divisor prj =
  object (self)
    inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)

    method! vexpr e =
      match e.enode with
      | BinOp ((Div | Mod), _, denom, _) ->
          (* 获取denom在新项目中的副本 *)
          let new_denom = Visitor_behavior.Get.expr self#behavior denom in
          let logic_denom = Logic_utils.expr_to_term ~coerce:false new_denom in
          let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
          let stmt =
            match self#current_kinstr with
            | Kglobal -> assert false
            | Kstmt s -> s
          in
          let kf = Option.get self#current_kf in
          let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
          Options.Self.result "NewStmt: %a" Printer.pp_stmt new_stmt;
          let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
          Queue.add
            (fun () ->
              Annotations.add_assert syntax_alarm ~kf:new_kf new_stmt assertion)
            self#get_filling_actions;
          DoChildren
      | _ -> DoChildren
  end

let execute () =
  ignore
    (File.create_project_from_visitor "syntactic check" (new non_zero_divisor))

内容的提问来源于stack exchange，提问作者Hovig