--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] integer overflow



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