問題タブ [klee]

私はクレーの新人です。

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

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

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

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

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

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

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

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

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

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

昨日、stackoverflowで質問したのですが、明確に記載していなかったので、質問の仕方を変えて、もしかしたら問題を明確にするかもしれません。まず、klee が提供する get_sign.c の例を変更unistd.hし、プログラムに含め、次のように関数sleep()を呼び出してスレッドを一時停止します。

" llvm-gcc" を使用して get_sign.c をコンパイルし、次に objectfileklee get_sign.oを実行すると、スレッドが一時停止しません。つまり、sleep()動作しません。get_sign.o を実行するときに引数を追加すると、このようklee --libc=uclibc get_sign.oになりますが、残念ながら、スレッドはまだ中断されず、さらに klee はエラーを報告し、

この問題を解決するにはどうすればよいですか? ありがとう！

ubuntu で cloud9 アプリケーションを実行しようとしています。ただし、makeコマンドでエラーが発生します

この問題を解決する方法を教えてください。

https://askubuntu.com/questions/441621/cloud9-application-is-giving-error-error-ld-terminated-with-signal-11-segmentからのPSアップデート

同じエラーが発生しています」collect2: error: ld terminated with signal 11 [Segmentation fault], core dumped

http://www.doc.ic.ac.uk/~dsl11/klee-doxygen/overview.html

バイナリのメモリをモデル化しようとしているので、KLEE がそれをどのように処理するかを確認したいと思います。しかし、概要から説明を理解するのに苦労しています。

簡単な説明と、これがどのように行われるかの簡単な例を得ることができますか?

にコンパイルWiresharkしたLLVM後、いくつかのライブラリにリンクし、それらも にコンパイルしましLLVMた。

私がリンクしたライブラリはlibwsutil、libzおよびlibpcap. ただし、KLEE は未定義関数の警告を表示しlibpcapます。

これらのフラグを使用して libpcap をコンパイルしました。

これらのフラグは、他のライブラリでも機能しました。

原因は何ですか？

ブースト バージョン 1.54 を 64 ビット Ubuntu 14.04.1 OS にインストールし、metaSMT で KLEE をコンパイルしようとしています。ただし、私の問題はKLEEとmetaSMTとは無関係であると思うため、質問のタイトルです。それにもかかわらず、エラーを再現するために必要な手順を提示します。

このステップの前に、STP を使用して KLEE を正常にビルドして実行しました。こちらの手順に従って、metaSMT を正常に構築しました。その後、metaSMT を使用して KLEE を構成しましたが、make ENABLED_OPTIMIZED=1コマンドを実行すると次のエラーが表示されます。

以前が発生した絶対パスはわかりませんがNo such file or directory、ファイルシステムを確認したところ、ファイル/usr/include/c++/4.8.2/tr1が含まれるディレクトリが 1 つありますunordered_map。std::tr1::さらに、ファイル名に追加された を取り除く方法がわかりません。どんな助けでも大歓迎です。

Ubuntu 12.04 で KLEE をビルドする必要があります。私はKLEEのウェブサイトの指示に従いました。私はLLVM 2.9を構築しました。しかし、klee-uclibc をインストールする必要があり、構成の過程で、動作する LLVM ビットコード コンパイラが見つからないというエラーが表示されました。これは、LLVM のビルドが失敗したということですか? 私は Linux が初めてで、テスト ツールも初めてです。どんな助けでも大歓迎です。