Update using Eva's new API (since Frama-C 25.0)
This is an update to the previous answer, using Eva's new API, available since Frama-C 25.0 (Magnesium); I left the original answer for users based on older Frama-C versions.
Using Eva's new API, the above answer can be written more succinctly:
(* Prints the value associated to variable [vi] before [stmt]. *)
let pretty_vi fmt stmt vi =
let req = Eva.Results.before stmt in
let cvalue = Eva.Results.(eval_var vi req |> as_cvalue) in
Format.fprintf fmt "%a -> %a@." Printer.pp_varinfo vi
Cvalue.V.pretty cvalue (* print mapping *)
(* Prints the state at statement [stmt] for each local variable in [kf],
and for each global variable. *)
let pretty_local_and_global_vars kf fmt stmt =
let locals = Kernel_function.get_locals kf in
List.iter (fun vi -> pretty_vi fmt stmt vi) locals;
Globals.Vars.iter (fun vi _ -> pretty_vi fmt stmt vi)
(* Visits each statement in [kf] and prints the result of Value before the
statement. *)
class stmt_val_visitor kf =
object
inherit Visitor.frama_c_inplace
method! vstmt_aux stmt =
(match stmt.skind with
| Instr _ ->
Format.printf "state for all variables before stmt: %a@.%a@."
Printer.pp_stmt stmt (pretty_local_and_global_vars kf) stmt
| _ -> ());
Cil.DoChildren
end
(* usage: frama-c file.c -load-script print_vals.ml *)
let () =
Db.Main.extend (fun () ->
Format.printf "computing value...@.";
Eva.Analysis.compute ();
let fun_name = "main" in
Format.printf "visiting function: %s@." fun_name;
let kf_vis = new stmt_val_visitor in
let kf = Globals.Functions.find_by_name fun_name in
let fundec = Kernel_function.get_definition kf in
ignore (Visitor.visitFramacFunction (kf_vis kf) fundec);
Format.printf "done!@.")
Note that the output is not identical; it is actually more condensed, as in, instead of printing e.g. score -> {{ NULL -> {0} }}, which means, for location score, the offset associated to the NULL base, that is, a constant value, is 0, it simply prints score -> {0}. It also prints minimum/maximum bounds according to the variable type (e.g. int __fc_errno was printed as an unbounded interval [--..--] with the previous code; here, it is printed as [-2147483648..2147483647] when using a machdep with 32-bit integers).
The new API also makes it easier to answer queries such as Is there also a way to get the values after the statement?: just use Eva.Results.after instead of Eva.Results.before.
Finally, for callstack-specific information, search for callstack in the src/plugins/value/utils/results.mli file. This file also contains some lenghty comments explaining the API, as well as a usage sketch.
