Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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