Изменение массива на месте с последующим использованием Verifiable C

Question

VST 1.7, Coq 8.5pl2.

У меня есть глобальный массив processingQVars, для которого я вызвал функцию для изменения на месте, изменив условие 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, который является объявленной переменной processingQVals_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 для его решения?

Спасибо