如何用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
相关产品推荐
相关产品推荐

