Вот конкретный пример как печатать, для каждой локальной и глобальной переменной, результат вычисляется по значению перед каждым утверждением в данной функции (читай функции снизу вверх):
open Cil_types
(* Prints the value associated to variable [vi] before [stmt]. *)
let pretty_vi fmt stmt vi =
let kinstr = Kstmt stmt in (* make a kinstr from a stmt *)
let lval = (Var vi, NoOffset) in (* make an lval from a varinfo *)
let loc = (* make a location from a kinstr + an lval *)
!Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval
in
Db.Value.fold_state_callstack
(fun state() ->
(* for each state in the callstack *)
let value = Db.Value.find state loc in (* obtain value for location *)
Format.fprintf fmt "%a -> %[email protected]" Printer.pp_varinfo vi
Locations.Location_Bytes.pretty value (* print mapping *)
)() ~after:false kinstr
(* 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 (self)
inherit Visitor.frama_c_inplace
method! vstmt_aux stmt =
(match stmt.skind with
| Instr _ ->
Format.printf "state for all variables before stmt: %[email protected]%[email protected]"
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 [email protected]";
!Db.Value.compute();
let fun_name = "main" in
Format.printf "visiting function: %[email protected]" 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 "[email protected]")
Это далеко от идеала, и выход чем просто с использованием Cvalue.Model.pretty state, но он может служить базой для дальнейших модификаций.
Этот скрипт был протестирован с помощью магния Frama-C.
Чтобы получить государству после с заявлением, просто замените параметр ~after:false в fold_state_callstack с ~after:true. В моей предыдущей версии кода использовалась функция, которая уже привязывала это значение для предварительного состояния, но такая функция не экспортируется для пост-состояния, поэтому мы должны использовать fold_state_callstack (что, кстати, более мощное, поскольку оно позволяет получить конкретную состояние за звонок).
Состояние, возвращаемое 'Db.Value.get_stmt_state', не является отображением от * переменных * к абстрактным значениям, но оно более сильное, чем это, поэтому почему-то немного сложнее получить значение для переменной. Тем не менее, комментарии в решении связанного вопроса, похоже, заключают, что он сработал. Не могли бы вы указать, какую версию Frama-C вы используете? – anol
@anol - это правильно. Если вас интересуют только значения скалярных переменных, просто поставьте '(Var x, NoOffset)' как аргумент 'lval'' lval_to_loc', считая, что 'x' является переменной Frama-C (' varinfo'), вы вас интересует. – byako
В комментарии, который вы упомянули, что это за текст: '(Kstmt stmt) lv' Что такое lv? Является ли Kstmt литой или что-то в этом роде? –