Плагин Frama-C: Разрешить значения массива

Question

Я работаю над фрейм-c-плагином, который должен разрешать значения всех видов varibles. Мне удалось вызвать указатели разметки, структуры и typedefs и напечатать соответствующие значения.

Теперь я борюсь с получением значений массива.

Вот мой подход до сих пор, описание ниже:

| 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), но не выводит (правильные) результаты.

Это почти правильный подход, или я делаю это совершенно неправильно? Может ли кто-нибудь дать мне несколько советов о том, как получить значения массива?

Если что-то неясно (поскольку сложно описать, что я хочу), сообщите мне, я изменю свой вопрос.

EDIT

Ожидаемый результат кодекса, как этот

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]={ } (также для других индексов), поэтому я просто не получаю результатов для этого вида доступа, который я использую.

Answer 1

я понял, как это сделать:

Хитрость была, что с Cil.integer, новая константа ехр может быть построен!

С Cil.integer Cil_datatype.Location.unknown act, я создал новый exp.

С этим exp я смог построить индекс-офсет. Затем я добавил это новое смещение к фактическому смещению массива. Это новое смещение было использовано для создания нового lval.

Посредством этого я получил доступ к массивам индексов.

Теперь мой выход выглядит нормально:

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, которое довольно печатает как .

Простейшим решением для вашего исходного кода было бы заменить packed вызовом на Cil.zero Cil_datatype.Location.unknown, но ваше собственное исправление в порядке.