--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on June 2009 ---
> 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