Поиск способов указать функциональную спецификацию Verifiable-c

Question

Я только начинаю работу с поддающимся проверке c и пытаюсь сгенерировать функциональные спецификации для написанного мною кода. Мой основной пример, с которым я работаю, это (код C) просто

int xor(int v1, int v2) {
  return v1 ^ v2;
}

и я испытываю затруднения, собирая раздел определения xor_spec.

Благодарю.

Answer 1

Definition xor_spec :=
 DECLARE _xor
 WITH v1 : int, v2: int
 PRE [ _v1 OF tint, _v2 OF tint]
    PROP () 
    LOCAL (temp _v1 (Vint v1); temp _v2 (Vint v2))
    SEP ()
 POST [ tint ]
    PROP() 
    LOCAL (temp ret_temp (Vint (Int.xor v1 v2))) 
    SEP().

В этой версии используются значения типа int, то есть 32-разрядные целые числа из модуля Int в CompCert. Обычно я люблю указывать свои функции на математических числах; этот стиль спецификации хотел бы:

Definition xor_spec2 :=
 DECLARE _xor
 WITH v1 : Z, v2: Z
 PRE [ _v1 OF tint, _v2 OF tint]
    PROP (0 <= v1 <= Int.max_unsigned; 0 <= v2 <= Int.max_unsigned) 
    LOCAL (temp _v1 (Vint (Int.repr v1)); temp _v2 (Vint (Int.repr v2)))
    SEP ()
 POST [ tint ]
    PROP() 
    LOCAL (temp ret_temp (Vint (Int.repr (Z.lxor v1 v2)))) 
    SEP().

Предостережение: я не пробовал ни одного из них через Coq, поэтому они могут иметь незначительные опечатки. И я недостаточно изучил Z.lxor, чтобы убедиться, что вы этого хотите.

Answer 2

Можете ли вы опубликовать код C? Из вашего последнего комментария видно, что у вас есть локальные переменные "tmp", "bit", "key", но я не вижу их в программе на Си.