You need to enable JavaScript to run this app.
优惠活动
大模型
产品
解决方案
定价
更多

如何用Frama-C获取关联语句并打印位置?PDG插件崩溃求助

Frama-C PDG模块PdgTypes.Pdg.Bottom崩溃问题求助

问题背景

我需要通过Frama-C获取关联语句并打印其位置,参考相关问题后,执行命令frama-c -pdg -load-module print_pdg.ml uniq-8.16.c运行OCaml代码时,触发了PdgTypes.Pdg.Bottom崩溃报错。我已添加异常处理代码,但仍有疑问,作为Frama-C新手,希望得到帮助。

报错信息

[from] Done for function check_file
uniq-8.16.c.cov.origin.c:7371:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function main
[pdg] ====== PDG GRAPH COMPUTED ======
[pdg] computing for function Frama_C_bzero
[from] Computing for function Frama_C_bzero
[from] Done for function Frama_C_bzero
[pdg] done for function Frama_C_bzero
[pdg] computing for function Frama_C_copy_block
[from] Computing for function Frama_C_copy_block
[from] Done for function Frama_C_copy_block
[pdg] done for function Frama_C_copy_block
[pdg] computing for function __argmatch_die
[pdg] warning: unreachable entry point (sid:969, function __argmatch_die)
[pdg] Bottom for function __argmatch_die
[kernel] Current source was: uniq-8.16.c.cov.origin.c:1686
         The full backtrace is:
         Raised at file "src/plugins/pdg_types/pdgTypes.ml", line 499, characters 19-31
         Called from file "src/plugins/pdg_types/pdgTypes.ml" (inlined), line 502, characters 32-48
         Called from file "src/plugins/pdg_types/pdgTypes.ml", line 506, characters 41-56
         Called from file "map.ml", line 270, characters 20-25
         Called from file "map.ml", line 270, characters 10-18
         Called from file "map.ml", line 270, characters 10-18
         Called from file "map.ml", line 270, characters 10-18
         Called from file "map.ml", line 270, characters 10-18
         Called from file "queue.ml", line 105, characters 6-15
         Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
         
         Unexpected error (PdgTypes.Pdg.Bottom).
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Phosphorus-20170501.
         Note that a version and a backtrace alone often do not contain enough
         information to understand the bug. Guidelines for reporting bugs are at:
         http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines

原print_pdg.ml代码

let () = Db.Main.extend (fun () -
    Globals.Functions.iter (fun kf -
        let pdg = !Db.Pdg.get kf in
        !Db.Pdg.iter_nodes (fun n -
            match PdgTypes.Node.stmt n with
            | None -
            | Some st -
              Format.printf "%a: %a@."
                Printer.pp_location (Cil_datatype.Stmt.loc st) Printer.pp_stmt st
          ) pdg
      )
  )

添加异常处理后的代码

let () = Db.Main.extend (fun ()  -
    Globals.Functions.iter (fun kf -
        let pdg = !Db.Pdg.get kf in
        !Db.Pdg.iter_nodes (fun n -
            try
            match PdgTypes.Node.stmt n with
            | None -
            | Some st -
              Format.printf "%a: %a@."
                Printer.pp_location (Cil_datatype.Stmt.loc st) Printer.pp_stmt st
            with
            | PdgTypes.Pdg.Bottom -
            | PdgTypes.Pdg.Top -
          ) pdg
      )
  )

内容的提问来源于stack exchange,提问作者BaiQi

相关产品推荐
方舟 Agent Plan

超全模态模型 × Harness 升级,最新支持 Deepseek-V4.1-Flash、GLM-5.3 系列、Doubao-Seedream-5.0-pro、Kimi-K3 (部分), 限时 9.9 元起

最近更新时间:2026.08.16 22:45:37