Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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