--- layout: fc_discuss_archives title: Message 93 from Frama-C-discuss on January 2014 ---
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