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] Value Analysis: signed_overflow in addition to division_by_zero warning

  • Subject: [Frama-c-discuss] Value Analysis: signed_overflow in addition to division_by_zero warning
  • From: marcel.gehrke at tu-harburg.de (Marcel Gehrke)
  • Date: Mon, 27 Jan 2014 14:41:13 +0100
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