当 Eva 不报告任何错误时，如何将 -werror 错误与代码问题相关联？答案

【问题标题】：How to associate -werror errors with code problem when Eva doesn't report any errors?当 Eva 不报告任何错误时，如何将 -werror 错误与代码问题相关联？
【发布时间】：2019-04-21 11:09:29
【问题描述】：

Frama-C werror 插件 (https://github.com/sylvainnahas/framac-werror) 在此代码中报告错误，但 Eva 没有报告任何问题。我已经尝试增加 Frama-C 的详细程度，但我仍然看不出问题出在哪里。我正在运行通过 opam 在 Mac OS 10.13.6 上安装的 Frama-C 18.0 (Argon)。

#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！）但我看不出它是什么。关于如何找出 Eva 对什么不满意的任何提示？

【问题讨论】：

标签： frama-c

【解决方案1】：

werror 插件在这里似乎有问题。请注意，它是一个旧插件，可能不再维护。（事实上，它甚至不能使用最新的 Frama-C 版本进行开箱即用的编译。）

我快速浏览了代码，发出警告是因为Werror 读取了my_assert_crash 中fprintf 调用的前提条件的可访问性状态。这个调用被 Eva 证明是无效的，并且可访问性状态接收到状态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

【讨论】：