arrays - Frama-C插件: Resolve array-values

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 与表达式选项一起使用来获取数组的长度。

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

我认为这个想法基本上是有道理的，但我不知道增量是否正确完成(值可以，或者乘以某个大小或其他东西)，或者其他东西不起作用。

程序编译(警告匹配不包括所有情况，这是无关紧要的，因为我只能使用表达式，不能使用 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

您的原始代码查询索引Index(inc, offset)的值，其中inc是Cil.increm Packed act，act 是当前索引，packed 是数组的大小。因此，您基本上是在查询 size+0、size+1 ... size-+(size-1)。所有这些偏移量都是无效的，因为它们超出了范围。这就是为什么您获得值 Cvalue.V.bottom ，它漂亮地打印为 。

对原始代码最简单的修复是通过调用 Cil.zero Cil_datatype.Location.unknown 来替换 packed，但您自己的修复就可以了。