[prev in list] [next in list] [prev in thread] [next in thread] 

List:       klee-dev
Subject:    Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid
From:       Frank Busse <f.busse () imperial ! ac ! uk>
Date:       2022-08-09 7:44:30
Message-ID: 20220809084430.43382384 () haengemotte ! localdomain
[Download RAW message or body]

Hi,


On Mon, 8 Aug 2022 18:24:27 -0700
Biqian Cheng <bchen158@ucr.edu> wrote:

> Did you rebuild it (make) in case it was wrong beforehand?
>
> Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON
> -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then
> "make -j2" to rebuild it.

I meant uclibc. There is a "make -j2" line in step 5:
https://klee.github.io/build-llvm11/

Here you are configuring KLEE. Do a "make clean" in KLEE's build
directory and call cmake with your options again but add the path to
your llvm-config-11:

-DLLVM_CONFIG_BINARY=<path>/bin/llvm-config-11

> Then check the LLVM version klee is linked against (e.g. ldd
>> <path>/bin/klee)  
> 
> 
> I used "ldd /usr/local/bin/klee", it gives me:
> 
> ...
> libLLVM-10.so.1 => /usr/lib/llvm-10/lib/libLLVM-10.so.1
> (0x00007f183c049000) libstdc++.so.6 =>
> ...
> Is this indicating I'm using LLVM-10, while I'm supposed to use
> LLVM-11?

Yes.

> and finally the build output of your program.bc (enable verbose mode
> for
> > make/...).  
> 
> 
> Does this mean make -j2?

Depending on the Makefile for that program you can run "make VERBOSE=1"
or use a hack like "make SHELL='sh -x'" to see what commands are
executed. If it's just a single C file and you are using clang
directly, you don't need that step.


Kind regards,

Frank

_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[prev in list] [next in list] [prev in thread] [next in thread]