I assume that you know how to write a function print_val
of type Db.Value.t -> unit
The following code, to be placed before your matching on a Set
instruction, will catch an access to an array at index e
match i with
(* Access to an array *)
| Set ((_, Index (e, _)), _, _) ->
let v = !Db.Value.access_expr (Kstmt s) e in
print_val v
(* End special case *)
| Set(lval,_,_) ->
print_value lval s
Alternatively, if you know the name of your variable, you can use the function Globals.Vars.find_from_astinfo
to find the corresponding varinfo vi
, and this code to query the contents of the varinfo.
open Cil_types
let vi_content stmt vi =
let lv = (Var vi, NoOffset) in
!Db.Value.access (Kstmt stmt) lv