0

VST 1.7，Coq 8.5pl2。

我有一个全局数组processesQVars我调用了一个函数来进行就地修改，将 SEP 条件从

data_at Ews (tarray tint 8)
      (map Vint
         [Int.repr 15; Int.repr 5463; Int.repr 12; Int.repr 75; Int.repr 231; Int.repr 1431; 
         Int.repr 735; Int.repr 134]) processedQVals

将 Int.repr 调用数组作为声明的processesQVals_contents变量，以

data_at Ews (tarray tint 8)
      (map Vint (fold2 Int.xor (map Int.repr processedQVals_contents) (Int.repr 4231))) processedQVals

我遇到的问题是我试图通过forward_call调用这个数组上的另一个函数。该策略产生了这个（显然无法证明的）目标。功能规范的前提条件如下，然后是不可证明的目标：

Definition checkArray_spec :=
  DECLARE _checkArray
WITH signedBits: val, originalBits: val, sh: share, 
     signedContents : list Z, originalContents : list Z, invKey : Z, size: Z
PRE [ _signedBits OF (tptr tint), _originalBits OF (tptr tint), _invKey OF tint, _size OF tint ]
      PROP  (readable_share sh; writable_share sh; 0 <= size < Int.max_signed; 
             size = Zlength signedContents; size = Zlength originalContents; 
             Forall (fun bit => Int.min_signed <= bit <= Int.max_signed) signedContents; 
             Forall (fun bit => Int.min_signed <= bit <= Int.max_signed) originalContents)
      LOCAL (temp _signedBits signedBits; temp _originalBits originalBits; 
             temp _invKey (Vint (Int.repr invKey)); temp _size (Vint (Int.repr size)))
      SEP   ((data_at sh (tarray tint size) (map Vint (map Int.repr signedContents)) signedBits);
             (data_at sh (tarray tint size) (map Vint (map Int.repr originalContents)) originalBits))

data_at Ews (tarray tint 8) (map Vint (fold2 Int.xor (map Int.repr processedQVals_contents) (Int.repr 4231)))
  processedQVals
|-- data_at Ews (tarray tint 8) (map Vint (map Int.repr processedQVals_contents)) processedQVals *
    fold_right sepcon emp Frame

是否必须更改前置条件中的 SEP 子句，或者有没有办法更改对forward_call的调用来处理它？

谢谢

4

0 回答 0