Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Some newbie questions about frama-c

  • Subject: [Frama-c-discuss] Some newbie questions about frama-c
  • From: dmentre at linux-france.org (David MENTRÉ)
  • Date: Thu, 24 Nov 2016 21:35:48 +0100
  • In-reply-to: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
  • References: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
Hello,

Le 2016-11-22 à 09:38, Michael Tandy a écrit :
> I have some (simplified) code I'm trying to prove with Frama-c and
> I've got a few questions.

What do you want to prove? With which Frama-C plug-in?

In case you want to prove absence of run-time error, Value analysis
plug-in does it once you have applied André's suggestion, i.e. replacing
\valid by \valid_read for const pointer arguments:
"""
--- serializer.c	2016-11-24 21:13:36.960872020 +0100
+++ serializer_fix.c	2016-11-24 21:16:53.584096612 +0100
@@ -31,7 +31,7 @@
     return evt;
 }

-/*@ requires \valid(e);
+/*@ requires \valid_read(e);
   @ requires \valid(data_out+(0..100));
   @*/
 void MessageTypeA_serialize(Message const * const e, uint8_t *data_out,
size_t *length_out) {
@@ -49,7 +49,7 @@
     //if (length_out != NULL) *length_out = 0;
 }

-/*@ requires \valid(data_in+(0..10));
+/*@ requires \valid_read(data_in+(0..10));
   @*/
 MessageTypeA * MessageTypeA_deserialize(uint8_t const *data_in, size_t
*length_out) {
     // TODO length in variable
@@ -106,4 +106,4 @@
         if (!equal) return i;
     }*/
     return 0;
-}
\ No newline at end of file
+}
"""

Command lines used:
  frama-c-gui -val serializer_fix.c
  frama-c -val serializer_fix.c


Please always report command line(s) used. Frama-C has a lot of plug-ins
with a lot of possible settings for each one of them.

For code like a serializer/deserializer, I would recommend sticking to
Value analysis. WP is more complex to use, would require more
annotations and, as shown by Virgile and André, is not that good on
bit-shifting code. Of course, with Value analysis, you are limited to
"just" proving absence of run-time errors. But in my humble opinion this
is already a very good result. :-)

Best regards,
david