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] Value Analysis: signed_overflow in addition to division_by_zero warning

Hello,

On Mon, Jan 27, 2014 at 2:41 PM, Marcel Gehrke
<marcel.gehrke at tu-harburg.de> wrote:
> The division-by-zero warnings are clear.

Indeed. Notice that option -remove-redundant-alarms will get rid of
the alarms in the 'if' block, as they are logically implied by the
first one.

> I do not understand the signed-overflow warning.
> Can you guys help me figure out why the signed-overflow warning was annotated?

This is due to an over-approximation in the function that handles
potential overflows. It fails to catch the fact that the result is
guaranteed to be undefined/bottom, and instead approximates the result
by supposing that it contains all possible integer values. This causes
the two alarms. The results are particularly odd because at the end of
this handling function, we intersect the inferred range by the range
before having treated the overflow. This results in bottom.

> Further, if the annotation is needed, why is it not also annotated before the if block?

The annotation is superfluous, and will not appear in the next
version. Thanks for noticing this imprecision and reporting it.

-- 
Boris