問題タブ [jpf]

テスト例で Java パス ファインダーを動作させようとしています。Eclipse の検証プラグインを使用すると、何らかの理由で動作しないようです。その後、run-JPF メソッドを使用しています。JPF は、gov.nasa.jpf.jvm のような外部クラスを使用しようとするまで機能しているようです。彼が見つからないようであることを確認してください。run メソッドのクラスパスに追加しようとしましたが、それでも同じ問題が発生します。どうすればよいですか?

私はJavaが初めてです。Java (KLOC) プログラムのバグを検出する必要があります。Javaパスファインダーを使用しています。commandline で実行していcmdます。コマンドの使用

知りたかったのですが、どうすればよいですか：

1. レース コンディションを取得する
2. デッドロックを検出
3. 制御を確認する
4. JPFの管理を検証、検索
5. 数値拡張のチェック

すべてコマンドラインで？例を使用して上記の質問に答えることができれば、本当に役に立ちます。

ありがとう

JPF を実行しようとしましたが、次のヌル ポインター例外が発生しました。

対応するコードは次のとおりです。

シンボリック文字列で Jpf を実行しようとしていますが、期待される出力が生成されません。以下は、私が試しているおもちゃのプログラムです。

.jpf ファイルは次のとおりです。

ネストされた if 条件内で、文字列比較の値を出力しています。文字列 s1、s2 が s3 と等しくない場合にのみ、print ステートメントを出力する必要があります。また、symbolic.debug=true を使用して PC を印刷しました

以下は、私が疑問を持っている出力のスニペットです。ここで、出力は、s1、s2 が等しく、同時に s3 と等しくないことを示しています。これはどのように可能ですか？また、印刷ステートメントに「s2.equals(s3)=true」と表示されている場合、プログラムは if ブロックに入るべきではありません。

String の代わりに int を使用すると、コードが機能します。助けていただければ幸いです。jpf 構成に何か不足があれば教えてください。前もって感謝します