Follow this question: How can I map frama-c CLI code to the original c statement? And how can I find the documentation of the api of the frama-c?
I used the Ocaml code mentioned in the question(ran frama-c with frama-c -pdg -load-module print_pdg.ml uniq-8.16.c
), but got this result:
[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
The Ocaml code in print_pdg.ml
is:
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
)
)
After I wrote the exception handling:
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
)
)
I'm a novice in frama-c, so please forgive me for any unclear expression, thank you in advance for your help!
The exception PdgTypes.Pdg.Bottom
indicates that there is no PDG for a function. This can be caused by a function that has not been analyzed, for example. Before calling !Db.Pdg.iter_nodes
, you should check that the PDG for kf
is not Top
or Bottom
.