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