Discussion:
Fatal Error in BVTypeCheck
Jingde Liu
2014-05-20 02:43:08 UTC
Permalink
Hi everyone,

I encounter the following problem when using KLEE to execute a simple
program.

The code of the program is as bellow:
________________________________________
int test(int x) {
int a;
if(x>100)
{
a = x / 100;
if(a > 10)
return x;
}
return 0;
}
_________________________________________
After ran it using KLEE, it showed this error:
Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length
But when I ran it using Cloud9, it was OK.
I don't know how to handle this problem.
Any help is truly appreciated.
Martin Nowack
2014-05-21 12:02:21 UTC
Permalink
Hi,

Can you write your setup of KLEE and which LLVM version you use?

What are the arguments to start KLEE?

Cheers,
Martin
Post by Jingde Liu
Hi everyone,
I encounter the following problem when using KLEE to execute a simple program.
________________________________________
int test(int x) {
int a;
if(x>100)
{
a = x / 100;
if(a > 10)
return x;
}
return 0;
}
_________________________________________
Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length
But when I ran it using Cloud9, it was OK.
I don't know how to handle this problem.
Any help is truly appreciated.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack-***@public.gmane.org
----------------------------------------------------
Jingde Liu
2014-05-21 13:14:04 UTC
Permalink
Hi,
I built and ran KLEE just by following the Getting Started webpage (
http://klee.github.io/klee/GetStarted.html), and I used LLVM 2.9.
The arguments I used when using KLEE to ran the program was as same as the
Tutorial One (http://klee.github.io/klee/Tutorial-1.html) that shows how to
run get_sign.c.
Thank you.
Post by Martin Nowack
Hi,
Can you write your setup of KLEE and which LLVM version you use?
What are the arguments to start KLEE?
Cheers,
Martin
Post by Jingde Liu
Hi everyone,
I encounter the following problem when using KLEE to execute a simple
program.
Post by Jingde Liu
________________________________________
int test(int x) {
int a;
if(x>100)
{
a = x / 100;
if(a > 10)
return x;
}
return 0;
}
_________________________________________
Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal
length
Post by Jingde Liu
But when I ran it using Cloud9, it was OK.
I don't know how to handle this problem.
Any help is truly appreciated.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
---------------------------------------------------
Martin Nowack
Research Assistant
Technische UniversitÀt Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden
Phone: +49 351 463 39608
----------------------------------------------------
Loading...