--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis: signed_overflow in addition to division_by_zero warning



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