--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2011 ---
Several persons on the list have said they were getting completely imprecise results {{ ANYTHING }} during the value analysis of some large and unavailable programs. They also were unable to reduce the issue to a smaller program that developers could have investigated. While working on something unrelated, I stumbled on one way to get {{ ANYTHING }}. This is the only understood way to get this behavior at this time. People who get this behavior are invited to check whether their large, unavailable programs are in fact doing this: short retshort(void) { return 12; } int pin; int main (int c, char **v) { pin = (*((int (*)())retshort))(); return (1+pin); } With Carbon 20110201+ patchlevel1: /usr/local/Frama-C_Carbon/bin/frama-c -val get_top.c ... [value] Values for function main: pin[bits 0 to 15] ? {12; } __retres ? {{ ANYTHING }} It was known that the value analysis was too lenient when it came to function pointer casts, but not that this could have this particular consequence. Note that the C99 standard allows casting a function pointer to another function pointer type, and casting it BACK TO THE ORIGINAL TYPE before calling the function, and nothing else. Programs that only do that are analyzed correctly and without {{ ANYTHING }}. In the next release, the above program will emit an alarm and be diagnosed as non terminating. Programs where the apparent call to retshort() is the consequence of an approximation by the value analysis, but which in fact use function pointers more carefully, will have the alarm and calls to function(s) with a better matching return type will be taken into account. Pascal