--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Fwd: Provide information to the value analysis



I post my message again since it seems that the previous one
didn't reach the list...

-------- Message original --------
Sujet: Provide information to the value analysis
Date : Thu, 12 Apr 2012 12:29:47 +0200
De : Anne Pacalet <anne.pacalet at free.fr>
Pour : Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>

Hello,

I was wondering if there is a way to write an ACSL annotation
to specify an external function returned value when it is
a pointer. I am trying to do something like:

int T[10];

/*@ ensures \result == \null || \result == T+i; */
extern int * fptr (int i);

int main (void) {
   int * p = fptr (3);
   if (p) *p = 0;
   return 0;
}

but I always get :
p ? {‌{ &NULL ; &alloced_return_fptr + [0..2147483644],0%4 }‌}

Doing the same thing for an 'int' seems to work:

/*@ ensures \result == 1 || \result == 5; */
extern int fint (int n);

gives: i ? {1; 5}

I also tried to add an assertion after the call :
   //@ assert p  == \null || p == T+3;
to split the analysis as explained in
http://blog.frama-c.com/index.php?post/2012/04/12/Helping-the-value-analysis-3
but it is not working either.

I know that a work-around is to write a dummy 'fptr' function...
but I would prefer if I could use an ACSL specification.

Thanks for your help.
-- 
Anne.