cdependenciesocamlframa-c

How to use frama-c to obtain the associated statements and then print their location


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!


Solution

  • 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.