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

Question

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?

标签： frama-c

Answer 1

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