--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on June 2009 ---
>> >> Running Frama-C's value analysis gives this: >> >> Values for function foo: >> tmp ? {0; } >> __retres ? {0; } >> >> If I understand correctly, this means that the function must return >> 0. > > For test programs that are destined to be both analyzed and executed, > I agree that our handling of printf is not the best. You can confirm > that > the temporary variable tmp indeeds holds the value of foo(-2) by > inspecting the normalized source code ("frama-c test.c -print"). And trying my own advice after sending it to the list, I realize that I got it wrong and that it is __retres that holds the return value of foo. Facepalm. Pascal -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090612/3a4cdf76/attachment.htm