前提条件中的数组范围

Question

我目前正在尝试学习如何使用 VST。我正在使用 VST 1.5。我有这个小 C 程序 (backref.c):

char* rbr (char* out, int length, int dist) {
  while (length-- > 0) { out[0] = out[-dist]; out++; }
  return out;
}

我的 Coq 代码（带有简单的前置条件和后置条件）是

Require Import floyd.proofauto.
Require Import backref.

Local Open Scope logic.
Local Open Scope Z.

Definition rbr_spec :=
  DECLARE _rbr
    WITH sh : share, contents : Z -> int
      PRE [ _out OF (tptr tuchar), _length OF tint, _dist OF tint ]
        PROP ()
        LOCAL ()
        SEP ()
      POST [tptr tuchar] local(fun _ => True).

作为前提，我想说out[-dist]到out[-1]是可读的，out[0]到out[length-1]是可写的。 PLCC 第 210 页讲述了一个条件 array_at_range，但它似乎在 VST 1.5 中不可用。我该怎么做？

Answer 1

您可以使用 array_at。但是因为你的数组的两个不同部分有不同的所有权份额，你必须将它们描述为两种不同的数组段。

类似于：

p: val  (* base address of array *)
v1: list val  (* contents of array segment 1 *)
v2: list val  (* contents of array segment 2 *)
sh: share (* readable *)
sh': share (* writable *)

SEP (`(array_at sh tint nil (-dist) (-1) v1 p);
     `(array_at sh' tint nil 0 (length-1) v2 p))

但比这更复杂，因为这省去了以下 (-dist) 和以上 (length-1) 部分的描述。

也许您不需要不同所有权的完全通用性共享数组的各个部分；你能想到为什么您的功能的客户需要这个吗？在这种情况下，只有一个数组段会更容易，其 "value" 是几个列表的串联。这说明在示例 progs/verif_revarray.v;特别注意到该文件中的 reverse_Inv。

前提条件中的数组范围

Array range in precondition

verifiable-c