ocaml - 在值分析中获取数组索引变量及其值(Frama-C)

Question

我想在 Frama-C 中查询值(value)分析插件以获取获取其值(value)的说明。对于每个数组，它返回整个数组的值范围。例如，如果指令是 array[i] = 1; , 我得到了结果 = {1}为 array[i]来自值(value)分析插件。现在，例如array[i] , 我想得到变量名 i及其值(value)分析的值(value)。

下面是我的代码示例

class print_VA_result out = object 
inherit Visitor.frama_c_inplace
     (**..*)
 method vstmt_aux s = 
  if Db.Value.is_computed () then
     match s.skind with
    | Instr i ->
       begin
         match i with
         | Set(lval,_,_) ->     
            print_value lval s
         |_ -> "<>"   
 ...

有人可以帮我吗？非常感谢。

Answer 1

我假设您知道如何编写函数 print_val类型 Db.Value.t -> unit下面的代码，要放在你匹配的前面Set指令，将捕获对索引 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

或者，如果您知道变量的名称，则可以使用函数 Globals.Vars.find_from_astinfo找到对应的varinfo vi , 这段代码用来查询 varinfo 的内容。

open Cil_types    

let vi_content stmt vi =
  let lv = (Var vi, NoOffset) in
  !Db.Value.access (Kstmt stmt) lv