Как связать ошибки -werror с проблемой кода, когда Eva не сообщает об ошибках?

Question

Подключаемый модуль Frama-C werror (https://github.com/sylvainnahas/framac-werror) сообщает об ошибке в этом коде, но Ева не сообщает о каких-либо проблемах. Я пытался увеличить многословность Frama-C, но все еще не мог понять, гдепроблема заключается в том, что я использую Frama-C 18.0 (Argon), установленную через операционную систему Mac OS 10.13.6.

#include <stdio.h>
#include <stdbool.h>
#include <stdlib.h>

#define MY_ASSERT(must_be_true__) \
(void)((must_be_true__) ? (void)0 : my_assert_crash())

void my_assert_crash() {
    fprintf(stderr, "my_assert_crash\n");  /* problem here? */
    exit(1);
}

int main(void) {
    MY_ASSERT(true);
    return 0;
}

Командная строка Frama-C и вывод для нее:

$ frama-c -c11 -machdep x86_64 assertion_no_diagnostic.c -eva -eva-slevel 10 -then -nonterm -then -werror -werror-no-external
[kernel] Parsing assertion_no_diagnostic.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  __retres ∈ {0}
[werror] Analysis reports 1 bug(s) (invalid and complete proofs). Aborting.

Однако, если я удалю строку fprintf, помеченную как «/ * проблема здесь? * /», Сообщение об ошибке исчезнет:

$ frama-c -c11 -machdep x86_64 assertion_non_fprintf_before_exit.c -eva -eva-slevel 10 -then -nonterm -then -werror -werror-no-external
[kernel] Parsing assertion_non_fprintf_before_exit.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  __retres ∈ {0}

Я чувствую, что делаю что-то глупое (особенно потому, чтоэто моя первая попытка использовать Frama-C!) но я не понимаю, что это такое. Какие-нибудь советы, как узнать, чем недовольна Ева?

Answer 1

Плагин werror здесь кажется неисправным. Обратите внимание, что это старый плагин, который, скорее всего, больше не поддерживается. (На самом деле, он даже не компилируется из коробки с последними версиями Frama-C.)

Я быстро взглянул на код, и выдается предупреждение, потому что Werror читает статус доступности предусловия вызова для fprintf в my_assert_crash. Ева завершила этот вызов, а статус доступности получает статус Invalid. Однако это не следует считать ошибкой, и Werror необходимо исправить. Я предлагаю вам применить следующий патч. Однако вы заметите, что по-прежнему будете получать ошибки, связанные с мертвым кодом.

diff --git a/inspector.ml b/inspector.ml
index 09d40fa..816ec2e 100644
--- a/inspector.ml
+++ b/inspector.ml
@@ -55,8 +57,9 @@ object(self)

   method statistics (ip:Property.t) st =
     begin
-      ignore(ip);
-      self#categorize st;
+      match ip with
+      | Property.IPReachable _ -> ()
+      | _ -> self#categorize st
     end

   method abort_on_error =

В целом, Werror нуждается в значительном обновлении. Мой совет - вместо этого использовать плагин Report, который интегрирован в дистрибутив Frama-C. Вы получите полный отзыв. Вот результат на вашем примере:

[...] many statuses

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
   135 Completely validated
   363 Considered valid
     1 Dead property
     1 Unreachable
   500 Total