Frama-C 插件：解析数组值

Question

我正在开发一个 frama-c 插件，它可以解析各种变量的值。我设法取消引用指针、结构和 typedef 并打印相应的值。

现在我正在努力获取数组的值。

这是我目前的方法，描述如下：

| TArray (typ, exp, bitsSizeofTypCache, attributes) -> (
    let len = Cil.lenOfArray exp in
    let rec loc_rec act max =
        if act < max then(              
            let packed = match exp with
            | Some x -> x
            in
            let inc = Cil.increm packed act in      
            let new_offset = (Index(inc, offset)) in
            rec_struct_solver typ (vi_name^"["^(string_of_int act)^"]") (lhost, new_offset);
            loc_rec (act+1) max
        );
    in
        loc_rec 0 len
)

我在匹配类型时通过使用带有表达式选项的 Cil.lenOfArray 设法获得了数组的长度。

现在我的方法是遍历数组的长度，增加描述表达式并修改偏移量，然后像处理局部变量一样处理变量（在下一个递归步骤中）。

我觉得这个思路基本上是有道理的，但是我不知道增量是否正确（值ok，或者乘以某个大小什么的），或者其他的东西不起作用。

程序编译（警告匹配不包括所有情况，这是无关紧要的，因为我只能使用表达式，而不是 NONE），但不输出 (正确）结果。

这是几乎正确的方法，还是我做的完全错了？有人可以给我一些关于如何获取数组值的提示吗？

如果有什么不清楚的地方（因为很难描述我想要什么），请告诉我，我会修改我的问题。

编辑

像这样的代码的预期结果

int arr[3];
arr[0]=0;
arr[1]=1;
arr[2]=2;
arr[0]=3;

应该是这样的：

arr[0]=0;3
arr[1]=1
arr[2]=2

我只是想通过程序获取数组每个索引处的所有值。虽然我只得到空结果，比如 arr[1]={ }（也适用于其他 Indizes），所以我根本没有得到我使用的这种访问的结果。

Answer 1

我知道怎么做了：

诀窍是，使用 Cil.integer，可以构建一个新的常量 exp！

使用 Cil.integer Cil_datatype.Location.unknown act，我创建了一个新的 exp。

有了这个 exp，我能够构建索引偏移量。然后我将这个新的偏移量添加到数组的实际偏移量中。这个新的偏移量用于构建一个新的 lval。

通过这样做，我获得了对数组 indizes 的访问权。

现在我的输出看起来不错：

arrayTest:arr[0]--->        0; 3
arrayTest:arr[1]--->        1
arrayTest:arr[2]--->        2

Answer 2

您的原始代码查询索引 Index(inc, offset) 的值，其中 inc 是 Cil.increm packed act，act 是当前索引，packed 是数组的大小。因此，您基本上是在查询 size+0、size+1 ... size-+(size-1)。所有这些偏移量都是无效的，因为它们是越界的。这就是为什么您获得值 Cvalue.V.bottom 的原因，它漂亮地打印为 </code>.</p> <p>对原始代码最简单的修复是通过调用 <code>Cil.zero Cil_datatype.Location.unknown 替换 packed，但您自己的修复没问题。

Frama-C 插件：解析数组值

Frama-C Plugin: Resolve array-values

arrays

frama-c