問題タブ [klee]

https://klee.github.io/tutorials/testing-coreutils/のステップ 3 に基づいて klee docker を使用して、LLVM で Coreutils を構築しようとしています。

しかし、実行時に問題が見つかりました：

それは言う

上記のコードを実行する前に、前に wllvm をインストールしました

そしてすでにインストールされています

しかし、私はすでにそれをインストールしましたが、それでもエラーが発生し、それを処理する方法がわかりません.Cコンパイラで提供されているソリューションを使用して、LLVMを使用したCoreutilsのビルド中に実行可能ファイルを作成できませんが、何も違いはありません.

その後、https://github.com/travitch/whole-program-llvm/issues/68の指示に従い、wllvm ではなく clang を使用すると言われています。その後、プログラムは実行されていましたが、実行時に再びエラーが発生しました

そう言う

ソースを検索しても、まだ解決できません。

これは wllvm が見つからないときの config.log の一部です

klee が少し前に行った実験を多少複製して、coreutils のコンパイル済みバイトコード バージョンで klee を実行しようとしています。

--max-time フラグの使い方がわかりません。

このコマンドを実行すると、最大時間が 10 秒であるにもかかわらず、約 3 分かかります。

このコマンドを実行すると、約 3 秒かかります。ファイル名と --max-time フラグが入れ替わっていることを除いて、コマンドは同じです。

最後に、 --max-time フラグなしで実行すると

少なくとも 30 分かかりますが、その時点であきらめて殺しました。

明らかに、ファイル名の前後のフラグはどちらも何かを行っていますが、何をしているのかわかりません。ドキュメントによると、 --max-time の標準的な使用法では、ファイル名の前に置きます。何が起こっているのか理解するのを手伝ってくれる人はいますか?