CODEWITHSUNDEEP
arraysframa-c
Thomas Böhm
Thomas Böhm

Reputation: 1486

Frama-C Plugin: Resolve array-values

I'm working on a frama-c plugin that should resolve the values of all kinds of varibles. I managed to dereference pointers and structs and typedefs and print the correspoinding values.

Now I'm struggling with getting the values of an array.

Here is my approach so far, description below:

| 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
)

I managed to get the length of the array by using Cil.lenOfArray with the expression-option when matching the type.

Now my approach is to go over the length of the array, increment the describing expression and modify the offset, and then handle the variable like a local variable (in the next recursion-step).

I think this idea basically makes sense, but I don't know if the increment is done correctly (value ok, or multiplied by some size or something), or other things don't work.

The program compiles (with the warning that the matching doesn't include all cases, which is irrelevant, since I can only work with expressions, not with NONE), but doesn't output the (correct) results.

Is this the nearly the right approach, or am I doing it completely wrong? Can someone give me some hints on how to get the array's values?

If something is unclear (since it is hard to describe what I want), please let me know, I will modify my question.

EDIT

The expected result of a Code like this

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

Should be something like that:

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

I simply want to get all the values at every index of the array over the program. While I get only empty results, like arr[1]={ } (also for the other Indizes), so I simply don't get results for this Kind of access I use.

Upvotes: 2

Views: 158

Answers (2)

byako
byako

Reputation: 3422

Your original code queries the value for the index Index(inc, offset), where inc is Cil.increm packed act, act is the current index, and packed is the size of the array. So you are basically making queries for size+0, size+1 ... size-+(size-1). All these offsets are invalid, because they are out-of-bounds. This is why you obtain the value Cvalue.V.bottom which pretty-prints as .

The simplest fix to your original code would have been to replace packed by a call to Cil.zero Cil_datatype.Location.unknown, but your own fix is fine.

Upvotes: 2

Thomas B&#246;hm
Thomas B&#246;hm

Reputation: 1486

I figured out how to do it:

The trick was, that with Cil.integer, a new constant exp can be built!

With Cil.integer Cil_datatype.Location.unknown act, I created a new exp.

With this exp, I was able to build an Index-Offset. Then I added this new offset to the actual offset of the array. This new offset was used to build a new lval.

By doing this, I got the access to the arrays indizes.

Now my output looks ok:

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

Upvotes: 1

Related Questions