4

我想查询 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
         |_ -> "<>"   
 ...

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

4

1 回答 1

7

我假设您知道如何编写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
于 2013-07-12T19:27:39.163 回答