--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on June 2009 ---
Thanks Pascal-- this patch is great and it seems to be working as expected! However the patched Frama-C is giving me some warnings about overflow for all of my little test functions (attached) except safe_signed_mul_1(). These test functions are supposed to be free of undefined behavior for all inputs, although of course there could be bugs in them. My guess is that the warnings are due to imprecision in Frama-C's value analysis. Precise analysis of bit-style code such as safe_signed_add_1() may be somewhat challenging for your abstract domains. However it would seem that purely arithmetic code such as safe_signed_add_2() should be analyzable using a framework like Frama-C. Are octagons sufficient to precisely analyze safe_signed_add_2()? I can't tell if something a bit more powerful is needed, such as the "decision tree abstract domain" described in the Astree PLDI paper. I am getting my test code from these pages, which are an excellent source of information about avoiding undefined behavior when doing math in C: https://www.securecoding.cert.org/confluence/display/seccode/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow https://www.securecoding.cert.org/confluence/display/seccode/INT34-C.+Do+not+shift+a+negative+number+of+bits+or+more+bits+than+exist+in+the+operand John -------------- next part -------------- A non-text attachment was scrubbed... Name: undef.c Type: text/x-csrc Size: 2209 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090612/88e1665e/attachment.c