--- layout: fc_discuss_archives title: Message 87 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 25/01/2014 21:17, Dharmalingam Ganesan a ?crit :
> For this below function, the value plugin says the
>
> [value] Values at end of function myFun:
>            i ? [--..--]
>
>
> In my understanding [--, --] refers to all possible integers. But, the value of i for this function can never be below zero.

In fact, Value analysis knows about this fact, see below 
"Frama_C_show_each_i([0..4294967295])".

Maybe Value prints "[--..--]" because the whole range of variable "i" is 
seen?

------------
unsigned int i = 0;

void myFun()
{
    i++;
    Frama_C_show_each_i(i);
}
-----------

$ frama-c -val unint.c -main myFun -lib-entry
[kernel] preprocessing with "gcc -C -E -I.  unint.c"
[value] Analyzing an incomplete application starting at myFun
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
   i ? [--..--]
unint.c:6:[value] assigning non deterministic value for the first time
[value] Called Frama_C_show_each_i([0..4294967295])
unint.c:8:[value] Assertion got status valid.
unint.c:3:[value] Function myFun: postcondition got status valid.
[value] Recording results for myFun
[value] done for function myFun
[value] ====== VALUES COMPUTED ======
[value] Values at end of function myFun:
   i ? [--..--]



In below int.c program (with an "int" instead of "unsigned int"), the 
Value analysis computes the correct range for i:

---------------
#include <limits.h>
int i = 0;

void myFun()
{
    if (i == INT_MAX) {
      i = 0;
    }
    i++;
    Frama_C_show_each_i(i);
}

void main(void)
{
   while (Frama_C_nondet(0,1)) {
     myFun();
   }
}
----------------

$ frama-c -val `frama-c -print-share-path`/builtin.c -slevel 10 int.c
[...]
[value] ====== VALUES COMPUTED ======
[value] Values at end of function Frama_C_nondet:
   Frama_C_entropy_source ? [--..--]
[value] Values at end of function myFun:
   i ? [1..2147483647]
[value] Values at end of function main:
   Frama_C_entropy_source ? [--..--]
   i ? [0..2147483647]


Best regards,
david