--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on January 2014 ---
Hey there, when i provide the value analysis the following code: void f1(int x) { int h; h = 1/x; if (x != 0) h = 1/x; else h = 1/x; } I use frama-c-Fluorine-20130601 and called it with Frama-C -val file main=f1 It produced the annotated code with the following warnings: void f1(int x) { int h; /*@ assert Value: division_by_zero: x ? 0; */ h = 1 / x; if (x != 0) /*@ assert Value: division_by_zero: x ? 0; */ h = 1 / x; else /*@ assert Value: division_by_zero: x ? 0; */ /*@ assert Value: signed_overflow: 1/x ? 2147483647; */ /*@ assert Value: signed_overflow: -2147483648 ? 1/x; */ h = 1 / x; return; } The division-by-zero warnings are clear. I do not understand the signed-overflow warning. Can you guys help me figure out why the signed-overflow warning was annotated? Further, if the annotation is needed, why is it not also annotated before the if block? Regards Marcel Gehrke