search

Quuxplusone / LLVMBugzillaTest

0 stars 0 forks source link

klee: Global.h:77: T* MINISAT::xrealloc(T*, size_t) [with T = MINISAT::Clause*]: Assertion `size == 0 || tmp != __null' failed. #4758

Closed Quuxplusone closed 9 years ago

Quuxplusone commented 15 years ago
Bugzilla Link PR4265
Status RESOLVED WONTFIX
Importance P normal
Reported by Daniel Dunbar (daniel@zuster.org)
Reported on 2009-05-25 15:42:53 -0700
Last modified on 2014-12-19 07:38:56 -0800
Version unspecified
Hardware PC All
CC c.cadar@imperial.ac.uk, edwin+bugs@etorok.eu, llvm-bugs@lists.llvm.org
Fixed by commit(s)
Attachments patch.txt (2061 bytes, text/plain)
Blocks
Blocked by
See also 
Reported by Török Edwin:
--
This is how I run klee:
~/llvm-svn/klee/Release/bin/klee -use-forked-stp  -const-array-opt
-libc=uclibc  -posix-runtime -init-env --use-batching-search
-randomize-fork --batch-time=30 x.bc -sym-files 1 283 A

This is how I configured klee:
./configure --with-llvmsrc=/home/edwin/llvm-svn/llvm
--with-llvmobj=/home/edwin/llvm-svn/llvm-obj32
--with-uclibc=/home/edwin/llvm-svn/klee/klee-uclibc

I'm using TOT llvm.

I had to patch klee to actually produce a useful symbolic file for me,
see attached patch.
Not sure if this is the correct approach, but I haven't seen any other way.

FWIW this is running on a Intel(R) Core(TM)2 Quad  CPU   Q9550  @
2.83GHz with 4G of RAM.

This is the output from running klee:

KLEE: NOTE: Using model:
/home/edwin/llvm-svn/klee/Release/lib/libkleeRuntimePOSIX.bca

KLEE: output directory =
"klee-out-62"

KLEE: WARNING: undefined reference to function:
pread

KLEE: WARNING: executable has module level assembly
(ignoring)

KLEE: WARNING: calling external: syscall(54, 0, 21505,
271070832)

KLEE: WARNING: calling __user_main with extra
arguments.

LibClamAV debug: Initialized devel-20090524
engine

LibClamAV debug: Initializing phishcheck
module

LibClamAV debug: Phishcheck: Compiling regex: ^
*(http|https|ftp:(//)?)?[0-9]{1,3}(\.[0-9]{1,3}){3}[/?:]?
*$
LibClamAV debug: Phishcheck module
initialized

LibClamAV debug: Loading databases from
/home/edwin/clam/git/builds/klee/pfx/share/clamav

LibClamAV debug:
/home/edwin/clam/git/builds/klee/pfx/share/clamav/main.hdb
loaded
Loaded 1
signatures.

LibClamAV debug: Initializing
engine->root[0]

LibClamAV debug: Initialising AC pattern matcher of
root[0]

LibClamAV debug: cli_initroots: Initializing BM tables of
root[0]
LibClamAV debug: Initializing
engine->root[1]

LibClamAV debug: Initialising AC pattern matcher of
root[1]

LibClamAV debug: cli_initroots: Initializing BM tables of
root[1]
LibClamAV debug: Initializing
engine->root[2]

LibClamAV debug: Initialising AC pattern matcher of
root[2]

LibClamAV debug: Initializing
engine->root[3]

LibClamAV debug: Initialising AC pattern matcher of
root[3]

LibClamAV debug: Initializing
engine->root[4]

LibClamAV debug: Initialising AC pattern matcher of
root[4]

LibClamAV debug: Initializing
engine->root[5]

LibClamAV debug: Initialising AC pattern matcher of
root[5]

LibClamAV debug: Initializing
engine->root[6]

LibClamAV debug: Initialising AC pattern matcher of
root[6]

LibClamAV debug: Initializing
engine->root[7]

LibClamAV debug: Initialising AC pattern matcher of
root[7]

LibClamAV debug: Initializing
engine->root[8]

LibClamAV debug: Initialising AC pattern matcher of
root[8]

LibClamAV debug: Loaded 104 filetype
definitions

LibClamAV debug: matcher[0]: GENERIC: AC sigs: 53 BM sigs:
0
LibClamAV debug: matcher[1]: PE: AC sigs: 0 BM sigs:
0

LibClamAV debug: matcher[2]: OLE2: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: matcher[3]: HTML: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: matcher[4]: MAIL: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: matcher[5]: GRAPHICS: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: matcher[6]: ELF: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: matcher[7]: ASCII: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: matcher[8]: DISASM: AC sigs: 0 BM sigs: 0 (ac_only
mode)
LibClamAV debug: Dynamic engine configuration
settings:

LibClamAV debug:
--------------------------------------

LibClamAV debug: Module PE:
On

LibClamAV debug:    * Submodule     PARITE:
On

LibClamAV debug:    * Submodule       KRIZ:
On

LibClamAV debug:    * Submodule    MAGISTR:
On

LibClamAV debug:    * Submodule    POLIPOS:
On

LibClamAV debug:    * Submodule    MD5SECT:
On

LibClamAV debug:    * Submodule        UPX:
On

LibClamAV debug:    * Submodule        FSG:
On

LibClamAV debug:    * Submodule    SWIZZOR:
On

LibClamAV debug:    * Submodule     PETITE:
On

LibClamAV debug:    * Submodule     PESPIN:
On

LibClamAV debug:    * Submodule         YC:
On

LibClamAV debug:    * Submodule     WWPACK:
On

LibClamAV debug:    * Submodule     NSPACK:
On

LibClamAV debug:    * Submodule        MEW:
On

LibClamAV debug:    * Submodule      UPACK:
On

LibClamAV debug:    * Submodule     ASPACK:
On

LibClamAV debug: Module ELF:
On

LibClamAV debug: Module ARCHIVE:
On

LibClamAV debug:    * Submodule        RAR:
On

LibClamAV debug:    * Submodule        ZIP:
On

LibClamAV debug:    * Submodule       GZIP:
On

LibClamAV debug:    * Submodule       BZIP:
On

LibClamAV debug:    * Submodule        ARJ:
On

LibClamAV debug:    * Submodule       SZDD:
On

LibClamAV debug:    * Submodule        CAB:
On

LibClamAV debug:    * Submodule        CHM:
On

LibClamAV debug:    * Submodule       OLE2:
On

LibClamAV debug:    * Submodule        TAR:
On

LibClamAV debug:    * Submodule     BINHEX:
On

LibClamAV debug:    * Submodule        SIS:
On

LibClamAV debug:    * Submodule       NSIS:
On

LibClamAV debug:    * Submodule     AUTOIT:
On

LibClamAV debug: Module DOCUMENT:
On

LibClamAV debug:    * Submodule       HTML:
On

LibClamAV debug:    * Submodule        RTF:
On

LibClamAV debug:    * Submodule        PDF:
On

LibClamAV debug:    * Submodule     SCRIPT:
On

LibClamAV debug:    * Submodule HTMLSKIPRAW:
On

LibClamAV debug:    * Submodule     JSNORM:
On

LibClamAV debug: Module MAIL:
On

LibClamAV debug:    * Submodule       MBOX:
On

LibClamAV debug:    * Submodule       TNEF:
On

LibClamAV debug: Module OTHER:
On

LibClamAV debug:    * Submodule  UUENCODED:
On

LibClamAV debug:    * Submodule     SCRENC:
On

LibClamAV debug:    * Submodule       RIFF:
On

LibClamAV debug:    * Submodule       JPEG:
On

LibClamAV debug:    * Submodule    CRYPTFF:
On

LibClamAV debug:    * Submodule        DLP:
On

LibClamAV debug:    * Submodule  MYDOOMLOG:
On

LibClamAV debug: Module PHISHING
On

LibClamAV debug:    * Submodule     ENGINE:
On

LibClamAV debug:    * Submodule    ENTCONV:
On

LibClamAV debug: Recognized MS-EXE/DLL
file

KLEE: increased time budget from 30 to
34.2632

klee: Global.h:77: T* MINISAT::xrealloc(T*, size_t) [with T =
MINISAT::Clause*]: Assertion `size == 0 || tmp != __null' failed.
0   klee
0x08aeda98

error: STP did not return successfullyKLEE: done: total instructions =
23436375
KLEE: done: completed paths =
1

KLEE: done: generated tests = 1
--
Quuxplusone commented 15 years ago

Attached patch.txt (2061 bytes, text/plain): Patch to klee

Quuxplusone commented 9 years ago

Closing old issues on this DB, as KLEE has now moved to GitHub (https://github.com/klee/klee). Please file a report on GitHub if there is still a problem.