Как написать спецификацию разделения глобальной переменной, используя проверяемый c

Question

Ниже приведен пример кода на языке C.

unsigned int  COUNTER;
unsigned int  get_counter(void) {
    COUNTER ++;
    return COUNTER;
}

Я написал основную спецификацию с использованием поддающегося проверке c (vst), но в конце проверки я сталкиваюсь с ошибкой "typecheck_error (deref_byvalue tint)". Может ли какой-нибудь орган сказать мне, как написать правильную спецификацию основания вышеупомянутого основания? Дело в том, как написать SEP() глобальной переменной.

(вот неправильный, пожалуйста, поправьте меня)

Definition get_counter_spec :=
 DECLARE _get_counter
  WITH v : Z, counter:val
  PRE []
        PROP  () 
        LOCAL (gvar _COUNTER counter)
        SEP   (data_at Ews tint (Vint (Int.repr v)) counter)
  POST [ tint ]
        PROP () 
        LOCAL(temp ret_temp (Vint (Int.repr (v+1))))
        SEP   (data_at Ews tint (Vint (Int.repr (v+1))) counter).

Answer 1

Ваша ошибка: в C-программе COUNTER объявлен как "unsigned int", но в вашем get_counter_spec вы используете "tint" вместо "tuint". С этим изменением доказательство проходит сразу же: функция запуска; сделать 4 вперед.

Наша ошибка: полученное вами сообщение об ошибке (в VST 2.0) совершенно бесполезно! Я добавлю отчет о проблеме, чтобы улучшить отчетность об ошибках в этом случае.