获取数组索引变量及其值分析(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查找相应的varinfo vi,并使用此代码查询varinfo的内容.

open Cil_types    

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