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



Your spec is wrong. Result is always (-1) even when i == 5 (which actually only occurs in lib-entry mode, otherwise i == 0).
And there is no RTE to check, as it can be confirmed by value.
	L.

Le 24 janv. 2014 ? 03:36, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> 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;
> }
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss