You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I'm using KLEE 3.0 via Docker. I came across lots of unexpected warning messages like this:
warning: Linking two modules of different target triples: 'get_sign.bc' is 'x86_64-unknown-linux-gnu' whereas '__uClibc_main.os' is 'x86_64-pc-linux-gnu'
Manually specifying the target triple may solve this problem. I wonder if this could be fixed globally in the construction of a Docker image.
Steps to reproduce
First, pull the docker image down and start a fresh container.
This is unfortunately a result of building uclibc (building with wllvm) differently than KLEE's bitcode files (building with clang directly).
As a result, the target triplets are slightly different:
'x86_64-unknown-linux-gnu' vs. 'x86_64-pc-linux-gnu'
In this case, they are compatible.
But it becomes a problem if bitcode files of different platforms/architectures are mixed that's why KLEE is warning about it.
@YikeZhou I'll close this issue but feel free to re-open it with related follow-up questions.
I think it would be an improvement in terms of usability to remove such warnings when they don't matter, but this is something that LLVM rather than KLEE warns about.
Description
I'm using KLEE 3.0 via Docker. I came across lots of unexpected warning messages like this:
Manually specifying the target triple may solve this problem. I wonder if this could be fixed globally in the construction of a Docker image.
Steps to reproduce
First, pull the docker image down and start a fresh container.
Then we need to find some input for KLEE.
The program doesn't matter here. So I choose
get_sign.c
as an example.Now we have the .bc file. We can invoke KLEE with the following command-line.
Note: I'm aware that the
--libc=uclibc
option is unnecessary here.It is only used to illustrate the warnings caused by this option.
KLEE complains about the mismatching targets.
Platform
I'm running Docker (with the WSL 2 backend) on a Windows PC.
The text was updated successfully, but these errors were encountered: