我正在开发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当匹配类型时，我设法通过与expression-option一起使用来获取数组的长度。
现在，我的方法是遍历数组的长度，增加描述表达式并修改偏移量，然后像局部变量一样处理变量（在下一个递归步骤中）。
我认为这个想法基本上是有道理的，但是我不知道增量是否正确完成（值确定，或者乘以某个大小之类的东西），或者其他事情不起作用。
程序编译（警告匹配不包括所有情况，这是不相关的，因为我只能使用表达式，不能使用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），所以我只是没有得到我使用的这种访问的结果。
我想出了怎么做：
诀窍在于，使用Cil.integer可以构建一个新的常数exp！
有了Cil.integer Cil_datatype.Location.unknown act，我创建了一个新的exp。
有了这个exp，我就能建立一个Index-Offset。然后，我将此新偏移量添加到数组的实际偏移量中。这个新的偏移量用于构建新的lval。
这样，我就可以访问数组indizes了。
现在我的输出看起来正常：
arrayTest:arr[0]---> 0; 3
arrayTest:arr[1]---> 1
arrayTest:arr[2]---> 2
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句