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

[Frama-c-discuss] NON TERMINATING FUNCTION when adding specification



Dear List,

I have a strange problem getting a :
[value] Values at end of function main:
           NON TERMINATING FUNCTION
on an application.

I tried to get the simplest example from it, and there it is :
-------------------------------------------------------
//@ assigns dest[0..]; ensures \result == dest;
extern char *str_add (char *dest, int val);

int main (void) {
   int t[10];
   char str[256];
   for (int i = 0; i < 10; i++) t[i] = i;
   for (int i = 0; i < 10; i++) str_add (str, t[i]);
   return 0;
}
-------------------------------------------------------
The strange thing is that, when I remove the `ensures` property
from `str_add` specification, the value analysis gives :
[value] Values at end of function main:
           t[0..9] ? [0..9] or UNINITIALIZED
           str[0..255] ? [--..--] or UNINITIALIZED
           __retres ? {0}
as expected.

So my question is : why is this property disturbing the analysis ?
Should I always give the smallest specification ?

Thanks a lot for you help and advises.
-- 
Anne.