Project

General

Profile

Actions

Bug #2705

open

BLAST knows something about huge integer numbers?

Added by Evgeny Novikov over 12 years ago. Updated over 12 years ago.

Status:
Open
Priority:
Low
Assignee:
-
Category:
-
Target version:
-
Start date:
04/04/2012
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

It turns out that BLAST incorrectly processes very huge integer number in comparison with CPAchecker. An example is in attachment. As usual there is also a real driver where the given error was encountered (it causes false positive).


Files

test2.c (291 Bytes) test2.c Example with huge integer number that causes BLAST false positive Evgeny Novikov, 04/04/2012 07:36 PM
drivers-block-virtio_blk.o.general.i (1.53 MB) drivers-block-virtio_blk.o.general.i Real driver that has the same problem Evgeny Novikov, 04/04/2012 07:36 PM
Actions #1

Updated by Pavel Shved over 12 years ago

Did you try using -sv-comp flag?

Actions #2

Updated by Evgeny Novikov over 12 years ago

Pavel Shved wrote:

Did you try using -sv-comp flag?

It didn't help.

Actions #3

Updated by Pavel Shved over 12 years ago

  • Status changed from New to Open
  • Priority changed from Normal to Low

OCaml doesn't support unsigned 64-bit integers. The maximum value of an integer constant is 2⁶³. See the documentation. In this case, the number is greater than 2⁶³, so BLAST represented it as a signed integer (-4095).

CIL, however, supports such values via its own custom arbitrarily long integers. If the code is processed bu CIL, it prints if (a > 0xfffffffffffff001UL) (maybe it's because it doesn't try to convert it to the OCaml's native integers).

Actions

Also available in: Atom PDF