問題タブ [program-slicing]

Frama-c から後方スライスを取得しましたが、動的スライスではなく静的スライスのように見えます。

動的後方スライスを取得するためのframa-cの特定のオプションはありますか?

特定の位置で配列要素の後方スライスを実行しようとしています。2 つの異なるソース コードを試しました。最初のものは（first.c）です：

次のコマンドを実行します。

frama-c-gui -slevel 10 -val -slice-return メイン ファイル.c

次の生成コードを取得します。

x と y が定義されていないため、これは問題ないようです。そのため、「res」は out_array の任意の位置にある可能性があります。私は次のコードで試しました：

与えられた結果はまったく同じでした。ただし、配列内の特定の位置を明示的に探しており、ループは独立している (並列化可能) ため、出力は次のようになると予想されます。

例から明らかかどうかはわかりません。私がやりたいことは、特定の配列位置について、どのステートメントがその最終結果に影響を与えるかを特定することです。ご支援いただきありがとうございます。

私が読んだところによると、 Indusはプログラムのどの部分が特定のプログラム ポイントのセットに影響を与えているか、または影響を受けているかを識別するプログラム スライサーであり、Kaveriは Indus プログラム スライス ライブラリを利用して Eclipse でスライスを実行するプラグインです。

このリンクhttp://forge.cis.ksu.edu/frs/?group_id=12から zip をダウンロードしました が、使い方がわかりません。このプラグインの使い方を知りたいですか？

ソースコード分析タスクを実行するために Wala Java Slicer を使い始めたところです。図書館の正しい使い方について質問があります。次のサンプルコードがあるとします。

Wala を使用してステートメントのスライスを計算するprintlnと、次のステートメントが得られます。

Wala でスライスを作成するために使用しているコードを以下に示します。

スライスにあると思われるステートメントがいくつかありますが、存在しません。

• ut = userType依存するメソッド呼び出しut.getInt()がスライスに含まれているにもかかわらず、 assign ステートメントが含まれていない
• の実装からのステートメントgetInt()は含まれていません。「手続き間」スライスを有効にするオプションはありますか? .class ファイルは、.class ファイルの作成に使用されるパスに含まれていることに注意してくださいAnalysisScope。

ご覧のとおり、依存オプションにDataDependenceOptions.NO_BASE_NO_HEAPandを使用しています。ControlDependenceOptions.NONEしかしFULL、両方に使用しても問題は解決しません。

私は何を間違っていますか？

プログラムで .java ファイルを分析するために、Soot をいじり始めたところです。私が読んだ限りでは、Soot はソース コード分析用の非常に強力なツールのようですが、オンラインで見つけた資料のほとんどは、それをコマンド ライン ツールとして使用することについて述べています。

特定のディレクトリにある .java ファイルからプログラムでクラスをロードし、プログラム依存グラフ (PDG) を構築し、プログラム スライスを実行する必要があります。Soot がスライスを提供しているかどうかはまだわかりませんが、PDG があれば自分で実装できます。

まず、以下のコードを使用してみました。

しかし、うまくいきません。呼び出しで数秒間立ち往生し、loadClassAndSupportその後、例外などを何も与えずに、プログラムが突然存在します。

誰かがプログラムで Soot を使用しようとした場合、他に設定する必要のあるオプションはありますか? または、プログラムで最初からSoot をセットアップするチュートリアルを教えてもらえますか?

C ファイルが与えられた場合、いくつかの基準について後方スライスを計算し、そのスライスを元のコードと比較したいと考えています。最初からスライシング プログラムを実装したくないので、このタスクに役立つと思われる Frama-C に慣れようとしました。

ただし、私の問題は、Frama-C のスライス プラグインが前処理された入力コードを変更するため、元のどの行がスライスにも表示されるかを識別するのが難しくなることです。

例：

入力ファイルtest1.c:

前処理されたファイル (によって生成frama-c test1.c -print -ocode test1_norm.c):

スライス ( によって生成frama-c -slice-calls func1 test1.c -then-on 'Slicing export' -print):

の署名がmain異なり、 の名前がfunc1に変更されたことに注意してくださいfunc1_slice_1。

スライスと（前処理された）オリジナルを（計算可能な差分に関して）より簡単に比較できるようにするために、その動作を抑制する方法はありますか？

Frama-Cのスライシング プラグインを使用して複数のアサーションをスライスすることは可能ですか?

たとえば、次のコードが与えられた場合:

両方のアサーションのスライスを取得したいと思います。

Prolog で次の問題を解決しようとしています。正しくコーディングしたと思いますが、クエリは単に false を返します。何を変えるべきかについて何かアドバイスはありますか？問題は次のとおりです。

「地元のベーグル屋であるベーグル アレーは、通勤途中にコーヒーとベーグルを求めて立ち寄る人々で、朝の通勤時間には常に賑わいを見せていました。毎朝その場で作りたてのベーグルは非常に人気があり、店にはおいしいコーヒーもあるという事実は、ケーキのアイシングのようなものでした! ベーグルアレーで働く人々は明るくフレンドリーで有能であったため、大勢の顧客にもかかわらず、待ち時間が長くなったり不快になったりすることはありませんでした. ジョーと彼の同僚の 4 人が今朝立ち寄って、みんなが絶賛していたことを見て、店がその評判に応えていることを知ってうれしい驚きを感じました. 各同僚の名前、トッピングのベーグルの種類、味とサイズを決定しますそれぞれ注文したコーヒーの量（小、中、大）。」

1. ブラッドはベーグルを手に入れましたが、それは小麦ではなく、何も入っていませんでした。ウォルトは小さなコーヒーを注文しました。

2. ミディアム サイズのコーヒーを飲んだ 2 人の同僚は、ヘーゼルナッツ味のコーヒーを飲んだ同僚と、ピーナッツ バターを使ったベーグルを食べた人でした。

3. バターではなくオニオンベーグルを手に入れた人は、フレンチバニラコーヒーも手に入れましたが、小さなサイズではありませんでした。

4. 5 人の同僚は、大きなコーヒーを手に入れたジョー、アマレット風味のコーヒーを手に入れた人、小麦のベーグルを手に入れた人、ベーグルに卵とベーコンを手に入れた人でした。

5. リックはブルーベリー ベーグルを注文しませんでしたが、コロンビア コーヒーを注文しました。アマレットコーヒーはチェダーベーグルと一緒に注文しましたが、ウォルトは注文しませんでした。

6. クリームチーズにはブルーベリーベーグルは付いていませんでしたが、大きなコーヒーが付いていました。ごまベーグルにはバターが付いていましたが、カルロスは注文しませんでした。

私が書いたプロローグコードは次のとおりです。

「ベーグル（X）」というクエリを実行すると思います。問題の解決策を教えてくれるはずですが、false を返します。何か不足していますか？よろしくお願いします！