Z3 Python では、BitVector V の 8 ビットを抽出するために、次のように実行できます。
Extract(7, 0, V)
ただし、私のプログラムでは V が定数になる場合があるため、その場合、コードは文字通り次のようになります。
Extract(7, 0, 0x87654)
残念ながら、上記のコードは 0x87654 が 32 ビットの BitVector.7 であることを指定していないため、これは間違っています。
1 つの解決策は、次のような一時変数を作成することです。
tmp = BitVec('tmp', 32)
tmp == 0x87654
Extract(7, 0, tmp)
ただし、これを機能させるには一時的なものを作成する必要があるため、これは少し面倒です。一時変数を作成せずに別の方法があるかどうか疑問に思っていますか? コードでインラインで 0x87654 を BitVector にキャストする方法はありますか?
どうもありがとう。