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

[Frama-c-discuss] integer overflow



> int foo(int y)
> {
>   return (((unsigned short)y*(unsigned short)-2)>=(y?0:y));
> }
>
> int main (void)
> {
>   printf ("%d\n", foo(-2));
>   return 0;
> }
>
> 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").

Please find included a patch for warning about signed overflows.
This should be considered as a "proof of concept" only, and
certainly NOT as a model of how to adapt the value analysis.
What should be an alarm (stored in the annotations database) is only
a warning.

The tests I made for this patch follow IN THEIR ENTIRETY:

int x,y,z1,z2,z3,z4;
unsigned a,b,c1,c2;

int foo(int y)
{
   return (((unsigned short)y*(unsigned short)-2)>=(y?0:y));
}

void main(){
   x = 2;
   y = 3;
   z1 = x + y;
   x = 2147483646;
   z2 = x + y;
   z3 = foo(-2);

   a = 2;
   b = 3;
   c1 = a + b;
   a = 4294967294U;
   c2 = a + b;
}


$ bin/toplevel.opt -val test.c
...
test.c:14: Warning: Overflow in arithmetic operation
...
test.c:6: Warning: Overflow in arithmetic operation
...
Values for function main:
   x ? {2147483646; }
   y ? {3; }
   z1 ? {5; }
   z2 ? [--..--]
   z3 ? {0; 1; }
   a ? {4294967294; }
   b ? {3; }
   c1 ? {5; }
   c2 ? {1; }

Are these the results you would like to see for this program?

Pascal



-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090612/2c1c9652/attachment.htm 
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: signed_overflow.patch
Type: application/octet-stream
Taille: 972 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090612/2c1c9652/attachment.obj 
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090612/2c1c9652/attachment-0001.htm