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

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



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.