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

> 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