--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with matrix pointer



Hi all,
Here is an example  simple_2.c
I am facing with the following issue :

float  *foo(float (*C)[2][2],float (*x)[2]){
 float (*matrix_C)[2][2] = C;
 float (*vector_x)[2] = x;
 float foo_var=0;
 int i=0, j=0;
 foo_var =(*vector_x)[j];
 //foo_var =(*matrix_C)[i][j];
 return (*x);
};

If foo_var = (*vector_x)[j]; then there is no problem with the command :
frama-c -jessie -wp-prover why3ide simple_2.c

However, if foo_var =(*matrix_C)[i][j]; I am getting the following error:
failure: typeOfLval: Mem on a non-pointer ((*matrix_C)[i])

I am fairly sure I missed something in the frama-c or jessie documentation.
Can somebody help me with this issue ?


-- 
Dragan Stosic
Senior developer at IBM
phone: 085-773-1050
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
Mulhuddart
Dublin 15
Ireland
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140126/3f2e8004/attachment.html>