小编use*_*482的帖子

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

有人可以帮我这个吗？非常感谢提前.