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



On Thu, Jan 23, 2014 at 9:25 AM, Nicholas Mc Guire <der.herr at hofr.at> wrote:

> On Thu, 23 Jan 2014, David MENTRE wrote:
>
> just for completenes here is the code used in the above runs:
> int main(int i)
> {
>   if (0 <= i  && i <= 10)
>   {
>      return -1;
>   }
>
>   if (i == 5)
>   {
>      /* can never reach here? */
>      return -2;
>   }
>
>   return 0;
> }
>
>
> Use option -slevel 20 -val in order for Frama-C's value analysis to
separate the execution paths where 0 > i, 0 <= i, ...:

$ frama-c -val -slevel 20 t.c
...
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  __retres ? {-1; 0}

There is only one value analysis option to know until you are an advanced
user, and it is this one. It is the first and only non-administrative
option used in the tutorial of the value analysis.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140123/8c38f617/attachment.html>