--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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