Как использовать Why3 доказательства в GUI Frama-C?

Question

Это похоже на глупый вопрос, но я в тупике. Я пытаюсь использовать Frama-C Sodium и Why3 0.86.1 (оба установлены через OPAM), чтобы доказать некоторые простые свойства. Рассмотрим эту программу (toy.c):

int main(void) {
    char *hello = "hello world!";
    /*@ assert \valid_read(hello+(0..11)); */
    return 0;
}

Я хочу доказать это утверждение, используя графический интерфейс Frama-C и Why3. Итак, я бегу frama-c-gui toy.c выберите "Why3 (ide)" в качестве средства проверки и запустите "Подтверждение аннотаций функций WP" в основной функции. (В качестве альтернативы: я перехожу на вкладку "Цели WP" и запускаю отсюда IDE Why3.) Появляется Why3, я вызываю средство проверки по своему выбору, чтобы все стало зеленым, сохранил сеанс и вышел из Why3, а затем в Frama ничего не происходит -C GUI: свойство по-прежнему помечено оранжевым /"попытался проверить, но не смог решить".

Как мне сказать Frama-C на самом деле использовать доказательства, представленные Why3? Сами доказательства, безусловно, есть: если я снова открою Why3, все будет зеленым, поэтому сессия была сохранена правильно. Кроме того, Frama-C знает, что что- то произошло: когда IDE Why3 открыта, на вкладке целей WP виден небольшой символ зубчатого колеса, и он исчезает, когда я закрываю Why3.

(Я понимаю, что это конкретное свойство может быть доказано Alt-Ergo без участия Why3, но мне нужно Why3 для более сложных задач.)

Answer 1

Спасибо за сообщение об ошибке. Предлагаемое исправление, похоже, работает.

Тем не менее, мы хотели бы более тесно интегрироваться с сеансами Why-3 и импортировать обратно в Frama-C, где проверяющие стороны выполняли каждое обязательство по подтверждению. Действительно, мы исправим ошибку во время этого рефакторинга.

Answer 2

Предварительный ответ самому себе: похоже, что парсер Frama-C для XML-файла сеанса Why3 не совпадает с XML-файлом, созданным Why3 0.86.1. Этот патч, кажется, исправляет это:

diff -ur frama-c-Sodium-20150201/src/wp/why3_session.ml frama-c-Sodium-20150201-hacked/src/wp/why3_session.ml
--- frama-c-Sodium-20150201/src/wp/why3_session.ml  2015-03-06 16:28:27.000000000 +0100
+++ frama-c-Sodium-20150201-hacked/src/wp/why3_session.ml   2015-09-17 21:35:30.717409735 +0200
@@ -160,6 +160,20 @@
   let name = string_attribute "name" elt in
   name

+let load_result parent_goal r =
+  match r.Xml.name with
+  | "result" ->
+      let status = string_attribute "status" r in
+      assert (parent_goal.goal_verified = false);
+      parent_goal.goal_verified <- (status = "valid")
+  | _ -> ()
+
+let load_proof parent p =
+  match p.Xml.name with
+  | "proof" ->
+      List.iter (load_result parent) p.Xml.elements
+  | _ -> ()
+
 let rec load_goal parent g =
   match g.Xml.name with
   | "goal" ->
@@ -168,7 +182,9 @@
       let mg =
         raw_add_no_task parent gname
       in
-      mg.goal_verified <- verified
+      mg.goal_verified <- verified;
+      (* hack for different(?) session file format *)
+      List.iter (load_proof mg) g.Xml.elements
   | "label" -> ()
   | s ->
       Wp_parameters.debug

Нет гарантий, что это будет работать для кого-то еще (или даже, что это правильно для моих собственных нужд, хотя я так думаю).

Любые разработчики Frama-C здесь, случайно, кто мог бы прокомментировать?