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



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.

If you use frama-c-gui, you'll see the code mark as dead (red background).


* Note that you code is a bit too specific, as we always have "i == 0" 
(i is a non volatile, global variable, initialized at 0 at the beginning 
of the program).

I would rather use this example:
"""
int main(int i)
{
   if (0 <= i  && i <= 10)
   {
      return -1;
   }

   if (i == 5)
   {
      /* can never reach here? */
      return -2;
   }

   return 0;
}
"""

In that case, Value analysis rightly found the code dead with parameter 
-slevel 2 (allow at most 2 different analysis paths, see doc for details):
   frama-c-gui -val -slevel 2 unreachable.c

$ frama-c -val -slevel 2 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 ? {-1; 0}  <---------------------- *HERE* Never -2


* Or you could also use option -lib-entry on your original code:

$ frama-c -val -slevel 2 -lib-entry unreachable.c
[kernel] preprocessing with "gcc -C -E -I.  unreachable.c"
[value] Analyzing an incomplete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
   i ? [--..--] <----- *HERE* Unknown value for i when main() is called
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
   __retres ? {-1; 0} <----- *HERE* Never -2


Best regards,
david