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



Hi,

On Mon, Jan 27, 2014 at 9:29 AM, David MENTRE <dmentre at linux-france.org> wrote:
> 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.

Value's manual is misleading on this point. When querying the value of
a l-value [--..--], means all possible integers *that fit within the
type*. Here, on your 32 bits unsigned value, this amounts to
[0..4294967295]. This is not a display artefact: for various (good)
reasons, [--..--] is exactly what Value stores internally.

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

Exactly. When you call a primitive such as Frama_C_show_each, [--..--]
is converted to the actual range. Another option is to use the
"Evaluate term" contextual menu, in order to evaluate 'i+0'.

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

Yes.

> 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]

Indeed. As [0..2147483647] does not cover the entire range for i (the
negative values are missing), we do not display [--..--].

To complicate matters further, notice that your guard
>    if (i == INT_MAX) {
>      i = 0;
>    }
is not needed to obtain those results. Since signed integer overflow
is an undefined behavior, the alarm emitted by Value on the line i++
is sufficient to guarantee that i will never become negative. Without
the 'if', the exact same values are inferred for i.

HTH,

-- 
Boris