--- layout: fc_discuss_archives title: Message 58 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, 23 Jan 2014, Pascal Cuoq wrote:

>    On Thu, Jan 23, 2014 at 9:25 AM, Nicholas Mc Guire <[1]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.
>
hmm... not quite
the reported value was

in the mail from David MENTRE
<snip>
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  __retres ??? {-1}  <---------------- *HERE*
<snip>

but that would actually be wrong - the {-1; 0} I can get but
never the {-1} - so it seems Im still missing something here ? 

thx!
hofrat