--- layout: fc_discuss_archives title: Message 56 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, David MENTRE wrote:

> Hello Dharmalingam,
>
> Le 23/01/2014 03:54, Dharmalingam Ganesan a ??crit :
>> I'm wondering whether Frama-C can report unreachable code without any annotation, for example, see the below code?
>
> * Yes using Value analysis plug-in:
>
> $ frama-c -val unreachable.c
> [kernel] preprocessing with "gcc -C -E -I.  unreachable.c"
> [value] Analyzing a complete application starting at main
> [value] Computing initial state
> [value] Initial state computed
> [value] Values of globals at initialization
>   i ??? {0}
> [value] Recording results for main
> [value] done for function main
> [value] ====== VALUES COMPUTED ======
> [value] Values at end of function main:
>   __retres ??? {-1}  <---------------- *HERE*
>
> Value analysis determines your function always returns -1.
>
Interesting - Don't see that result !

hofrat at debian:~/frama-c$ frama-c -version
Version: Nitrogen-20111001
Compilation date: Wed May 16 13:02:51 UTC 2012
Share path: /usr/share/frama-c (may be overridden with FRAMAC_SHARE variable)
Library path: /usr/lib/frama-c (may be overridden with FRAMAC_LIB variable)
Plug-in paths: /usr/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)
hofrat at debian:~/frama-c$ frama-c -val unreachable.c
[kernel] preprocessing with "gcc -C -E -I.  unreachable.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
          __retres ? {-2; -1; 0} 

and florine also did not produce that result

hofrat at rtl15:~/frama-c$ frama-c -version
Version: Fluorine-20130401
Compilation date: Sun Jan 12 12:52:44 EST 2014
Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable)
Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable)
Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)
hofrat at rtl15:~/frama-c$ frama-c -val unreachable.c
[kernel] preprocessing with "gcc -C -E -I.  unreachable.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
          __retres ? {-2; -1; 0}

what version is this result from ?
or did I miss something essential ?

thx!
ofrat

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;
}