[klee-dev] Fatal Error in BVTypeCheck

[Jingde Liu]

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.


2014-05-21 20:02 GMT+08:00 Martin Nowack <martin_nowack at tu-dresden.de>:

> Hi,
>
> Can you write your setup of KLEE and which LLVM version you use?
>
> What are the arguments to start KLEE?
>
> Cheers,
> Martin
>
>
> On 20 May 2014, at 04:43, Jingde Liu <liujingde2008 at gmail.com> wrote:
>
> > 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.
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > 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 at tu-dresden.de
> ----------------------------------------------------
>
>
-------------- next part --------------
HTML attachment scrubbed and removed