在值分析中获取数组索引变量及其值（Frama-C）

Question

我想查询 Frama-C 中的价值分析插件以获取获取其价值的说明。对于每个数组，它返回整个数组的取值范围。例如，如果指令是array[i] = 1;，我从价值分析插件中得到 result = {1} for array[i]。现在，例如array[i]，我想通过值分析得到变量名i及其值。

下面是我的代码示例

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找到对应的varinfovi，这段代码查询varinfo的内容。

open Cil_types    

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