--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2016 ---
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