How to associate -werror errors with code problem when Eva doesn't report any errors?

The Frama-C werror plugin (https://github.com/sylvainnahas/framac-werror) reports an error in this code, but Eva doesn't report any problems. I've tried increasing Frama-C's verbosity but I still couldn't see where the problem lies. I'm running Frama-C 18.0 (Argon) installed via opam on 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;
}

The Frama-C command line and output for this is:

$ 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.

However if I remove the fprintf line that's marked as "/* problem here? */", the error message disappears:

$ 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}

I feel like I'm doing something dumb (especially because this is my first attempt to use Frama-C!) but I can't see what it is. Any tips on how to find out what Eva is unhappy about?

Solution

The werror plugin seems to be faulty here. Please note that it is an old plugin, that is likely not maintained anymore. (In fact, it does not even compile out-of-the-box with recent Frama-C versions.)

I had a quick glance at the code, and the warning is emitted because Werror reads the accessibility status of the precondition of the call to fprintf in my_assert_crash. This call is proven dead by Eva, and the accessibility status receives a status Invalid. However, this should not be counted as an error, and Werror must be patched. I suggest that you apply the following patch. However, you will notice that you will still obtain errors related to dead code.

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 =

Overall, Werror needs to be updated in a significant way. My advice is to use the Report plugin instead, which is integrated in the Frama-C distribution. You will get a complete feedback. Here is the result on your example:

[...] many statuses

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