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

[Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)



Hello Dharma,

I think your function satisfies its contract.
So, what shall Frama-C do?

Maybe, your issue is that the function also satisfies the following simpler contract?

Jens

int MAX_VALUE = 100;

float x = 0.0;

int status = 0;

/*@
  requires MAX_VALUE == 100;
  assigns status;
  ensures status == -1;
*/
int main()
{

  if((x > MAX_VALUE) ||
     (x <= MAX_VALUE))
  {
     status = -1;
  }
}