Спецификации с адресуемыми локальными переменными

Я пытаюсь понять, как VST обрабатывает (адресуемые) локальные переменные, поэтому я написал эту функцию:

int main() {
    int x = 5, y = 7;
    int *a = &x;
    int *b = &y;

    *a = 8;
    *b = 9;

    return x;
}

Затем я попытался проверить это с помощью следующей спецификации:

Definition main_spec :=
 DECLARE _main
  WITH p : int (* still toying with things, couldn't figure out how to drop this *)
  PRE [ ]
   PROP ()
   LOCAL ()
   SEP ()
  POST [ tint ]
   EX i : Z,
   PROP ( i = 8 )
   LOCAL (temp ret_temp  (Vint (Int.repr i)))
   SEP ().

Все идет хорошо, просто используя (forward) до возврата заявления, где я остался доказать следующее

data_at Tsh tint (vint 9) v_y * data_at Tsh tint (vint 8) v_x |-- FF

кажется, это должно быть недоказуемым (обратите внимание, что я только что применил forward до этого момента). Я ожидал, что какая-то спецификация скажет, что куча пуста после того, как локальные переменные были перераспределены, т.е. emp |-- emp,

Есть ли где-нибудь, что я мог бы посмотреть, чтобы получить больше информации об этом?

Спасибо!

Дополнительная информация: я копался в источнике FF пост-состояние, и оно исходит от typecheck_exprВ частности, дело за Evar:

  | Evar id ty =>
      match access_mode ty with
      | By_reference =>
          match get_var_type Delta id with
          | Some ty' =>
              tc_bool (eqb_type ty ty')
                (mismatch_context_type ty ty')
          | None =>
              tc_FF
                (var_not_in_tycontext Delta id)
          end
      | _ => tc_FF (deref_byvalue ty) (* ?? *)
      end

Если я не читаю что-то не так, это говорит о том, что вы не можете получить доступ к локальным переменным по значению. Это просто недосмотр? Или в семантике есть что-то, что этому мешает?

Источник

2 ответа

Решение

Причина этой неудачи в том, что вы забыли -normalize флаг к Clightgen. Если вы переведете свой .c использование файла clightgen -normalize вместо clightgen, это должно работать нормально.

Источник

Какую версию VST вы используете? В недавней версии master-branch (commit 506f8e7) следующее прямое доказательство работает просто отлично.

Lemma body_main: semax_body Vprog Gprog f_main 
main_spec.
Proof.
start_function.
forward.
forward.
forward.
forward.
forward.
forward.
forward.
forward.
Exists 8.
entailer!.
Qed.
Источник
Другие вопросы по тегам