CODEWITHSUNDEEP
graphstatic-analysisframa-c
Seongmin Lee
Seongmin Lee

Reputation: 3

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'm trying to get the program dependence graph (PDG) using frama-c at the original code's statement level. However, 'pdg' plug-in in frama-c prints the PDG at the parsed code's node level.

Since frama-c-gui can highlight the original statement corresponds to the node in the parsed code, I'm pretty sure that there is a mapping between the node in parsed code and the original code's statement. How can I get this mapping? Just the line number at the original code is fine, too.

Upvotes: 0

Views: 236

Answers (1)

anol
anol

Reputation: 8953

Frama-C's GUI presents two views of the code:

  1. The CIL code (C Intermediate Language), often called normalized source code, which corresponds to a pretty-printing of Frama's AST, in the top center panel;
  2. And the original source code, on the top right panel.

I'm assuming that by parsed code you are talking about the CIL (normalized) code.

Every element in Frama-C's AST contains a location, which is a pair of positions: the first and last coordinates (line, row, column) in the original code which correspond to that element (minus a few exceptions, such as generated elements, macro expansions, etc). Most AST elements have ways to retrieve that location.

In the case of PDG nodes, you can get the associated statements (if any) and then print their location, as in the code below (run with frama-c -pdg -load-module print_pdg.ml <file>):

(* 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
      )
  )

Note that my example script will print each statement multiple times, if there are multiple PDG nodes associated to the same statement.

By default, Printer.pp_location only prints the file name and line of the starting character, but you can make a custom pretty-printer to include the column as well, or the coordinates of the last character.

API and Plug-in Documentation (from question in comment)

Some Frama-C plug-ins (Eva, WP, E-ACSL, etc.) have their own manuals, which are available in the Frama-C download page.

There is no specific manual for the Pdg plug-in, but some Ocamldoc-generated HTML pages can be obtained from the Frama-C API archive.

However, what most Frama-C plug-in developers prefer is to use the OCaml Merlin plug-in in their favorite editor (emacs, vim, etc) to navigate the code and read the source comments (in the .mli files, for instance).

On Emacs, for instance, C-c C-l on a module/variable name jumps to its definition, and C-c C-a alternates between .ml and .mli files (implementation - documentation). Combined with auto-completion for module/function discovery, this provides a form of interactive documentation that many OCaml developers are comfortable with.

Upvotes: 2

Related Questions