[klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)

[Ming-Hsien Tsai]

We rebuilt KLEE again and now it works with the latest version of STP.
KLEE with STP-r940 is still not working but this should be fine now as
we have a working version. Thank you all for the suggestions.

If you are interested in our configuration and how we build and run
KLEE, it is detailed below. All the used scripts and patches are
attached.

Machine #1: Ubuntu 13.04 64bit with gcc 4.7.3
Machine #2: Ubuntu 14.04.2 LTS 64bit with gcc 4.8.2
(All installed packages are up-to-date.)

Assumptions:
  - All dependencies are installed.
  - The following files are placed in the same place with the scripts.
    * llvm-2.9.tgz
    * llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
    * stp-r940.tar.gz

Building Procedure:
  $ ./rebuild-llvm-gcc
  $ ./rebuild-llvm
  $ ./rebuild-stp-r940
  $ ./rebuild-stp-git
  $ ./rebuild-klee-uclibc
  $ ./rebuild-klee-r940
  $ ./rebuild-klee-git
  On Machine #2, I have to copy all .bca files in
klee-*/Release+Asserts/lib from Machine #1. (I don't know why these
files are missing on Machine #2.)

Executing KLEE: Use either run-klee-r940 or run-klee-git.

On both machines, the error occurs when running run-klee-r940 on the
example. run-klee-git works fine on both machines.


--
Ming-Hsien
-------------- next part --------------
A non-text attachment was scrubbed...
Name: llvm-2.9-gcc.patch
Type: application/octet-stream
Size: 615 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-klee-git
Type: application/octet-stream
Size: 1034 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-klee-r940
Type: application/octet-stream
Size: 894 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-klee-uclibc
Type: application/octet-stream
Size: 787 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0003.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-llvm
Type: application/octet-stream
Size: 450 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0004.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-llvm-gcc
Type: application/octet-stream
Size: 150 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0005.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-stp-git
Type: application/octet-stream
Size: 519 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0006.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rebuild-stp-r940
Type: application/octet-stream
Size: 537 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0007.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: run-klee-git
Type: application/octet-stream
Size: 892 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0008.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: run-klee-r940
Type: application/octet-stream
Size: 718 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0009.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: stp-r940-bison3.patch
Type: application/octet-stream
Size: 1714 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150306/e7f6770f/attachment-0010.obj>