--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on April 2012 ---
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.