:実行を開始します

レジスタビューを使用して、アクティブ状態のレジスターの値を視覚化できます。レジスタの値は、ダブルクリックすることで変更できます。右クリックメニューを使用すると:

メモリビューを使用して、アクティブ状態のメモリの一部の値を視覚化できます。 「モニターメモリ」をクリックすると、ユーザーは監視するメモリアドレスを指定できます。ウィジェットには、そのアドレスから始まる512バイトが表示されます。メモリビューは、ヘックスビューとASCIIビューの2つのセクションに分割されています。 HexViewは、バイトがマッピングされてコンクリートがマッピングされている場合にのみ、各バイトの六角値を表示します。バイトがマップされていない場合、チャラクタッド_が表示されます。バイトがシンボリックである場合、ウィジェットには文字が表示されます. 。
右クリックメニューを使用すると:
このウィジェットにより、シンボリックデータを含むバッファーを作成できます。
Pythonシェルを介してより多くのAPIを実行できます。たとえば、ソルバーを使用して、現在の状態の条件を証明できます。
> >> import borzacchiello_seninja as seninja
> >> s = seninja . get_current_state ()
> >> s . solver . satisfiable ( extra_constraints = [ s . regs . eax == 3 ])コードは、アクティブ状態のパス制約を考慮してeax == 3の満足度を確認します。
コマンドに関する詳細を確認するには、Wikiに相談してください。
Seninjaは、シンボリックエンジンの多くの部分を構成する可能性をユーザーに提供します(例:ページの次元、シンボリックメモリアクセス戦略など)。 Edit/Preferences/Settingsをクリックし、左ウィジェットでSENinja選択することにより、利用可能なすべての設定にアクセスおよび変更できます。
でテスト
4.03.114.8.14それを機能させるには、PIPにZ3をインストールする必要があります: $ pip3 install z3-solver