VST バージョン 1.7。
関数呼び出しで変数を使用しようとすると、coq がローカルで宣言された変数を認識しないという問題があります。私はコードを持っています：
void deSignArray(int bits[], int invKey, int size)
{
int i = 0;
while (i < size) {
int bit = bits[i];
int ans = deSignInt(bit, invKey);
bits[i] = ans;
i++;
}
}
coq タイプのビット: リスト Z、invKey: Z、サイズ: Z。
bit = bits[i] ステップを正常に実行しましたが、次に使用して前進しようとすると
forward_call((Int.repr bit), (Int.repr invKey)).
このステップは、環境内でビットが見つからずに失敗します。使ってみた
forward_call(_bit, (Int.repr invKey)).
_bit が LOCAL 句に表示されますが、_bit は int または Z 型ではなく ident 型であるため、型の不一致が生じます。結果として、ローカルで定義された値を使用して他の関数を呼び出す方法を考えているので、助けていただければ幸いです。