c - KLEE WARNINGS および入力が生成されない

Question

私はクレーの新人です。

クレーをインストールし、指示に正しく従いました。

チュートリアルからプログラムを実行した場合:

int get_sign(int x) {
if (x == 0)
   return 0;
if (x < 0)
   return -1;
else 
   return 1;
}

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
} 

期待どおりの結果が得られます:

KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 51
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3 

しかし、プログラムを実行したい場合は、次のようになります。

 urmas-PBL21 src # llvm-gcc -emit-llvm -c -g  tcas/versions/v1/tcas.c
 urmas-PBL21 src # klee  --libc=klee tcas.o
 KLEE: output directory = "klee-out-16"
 KLEE: WARNING: undefined reference to function: __errno_location
 KLEE: WARNING: undefined reference to function: fprintf
 KLEE: WARNING: undefined reference to variable: stdout

 KLEE: done: total instructions = 11
 KLEE: done: completed paths = 1
 KLEE: done: generated tests = 1

そして、入力は生成されません。

現在の klee のインストールは C 関数をサポートしていないようですが、チュートリアルに書かれているとおりにインストールしました: http://klee.llvm.org/GetStarted.html#build

uclibc と POSIX 環境モデルを使用すると、関数も処理できるようになります。

誰かがそれを手伝ってくれますか？

---

そして、クレーの実行中に --libc=klee を使用しないと、

urmas-PBL21 src # klee   tcas.o
KLEE: output directory = "klee-out-19"
KLEE: WARNING: undefined reference to function: atoi
KLEE: WARNING: undefined reference to function: fprintf
KLEE: WARNING: undefined reference to variable: stdout

KLEE: done: total instructions = 11
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

同じエラー、その他の警告。