Project

General

Profile

Actions
Copy link

Bug #2705

open

BLAST knows something about huge integer numbers?

Added by Evgeny Novikov about 12 years ago. Updated about 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

Download all 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
Copy link
 #1

Updated by Pavel Shved about 12 years ago

Did you try using -sv-comp flag?

Actions
Copy link
 #2

Updated by Evgeny Novikov about 12 years ago

Pavel Shved wrote:

Did you try using -sv-comp flag?

It didn't help.

Actions
Copy link
 #3

Updated by Pavel Shved about 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
Copy link

Also available in: Atom PDF