--- layout: fc_discuss_archives title: Message 68 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?



Hi,

Thanks for all responses. I'm not sure why the following code cannot considered invalid; I always get "unknown".

Any comments?

frama-c -wp -wp-rte non_sense.c -lib-entry



int i = 0;

/*@
  @ behavior BUG:
  @  assumes i == 5;
  @  ensures \result == -2;
*/

int main()
{
  if (0 <= i  && i <= 10)
  {
     return -1;
  }

  if (i == 5)
  {
     return -2;
  }

  return 0;
}