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: framacdisc at mjt.me.uk (Michael Tandy)
  • Date: Tue, 22 Nov 2016 08:38:52 +0000
I have some (simplified) code I'm trying to prove with Frama-c and
I've got a few questions. The code I'm working on converts structs to
and from byte arrays - serializing and deserializing - and I want to
prove that serializing then deserializing produces an identical struct
regardless of what's in the input struct's fields. You can see my code
here: https://gist.github.com/michaeltandy/31cd1cf582e9e2bae7e369c04606f128

The questions I've run into are:


1. What are the meanings of the GUI symbols Red-orange ball, green-red
ball, blue circle, yellow ball, green ball etc? I assume the green
ball indicates successful verification of the line, and all the others
something else? It would be nice if they displayed tool tips on
mouseover :)


2. In value analysis, what does <BOTTOM> mean? For example, in
MessageTypeA_serialize copying the pointer data_out to the pointer out
appears to change both values to <BOTTOM>


3. How does one assert that a method returns a valid pointer? I've
tried the following guesses without success:

/*@ assigns \valid(\result); */

//@ predicate valid_return(void *p) = \valid(p);
#define VALID_RETURN __attribute__((valid_return))
MessageTypeA * NON_NULL allocate() {

//@ predicate valid_return(void *p) = \valid(p);
#define VALID_RETURN __declspec(valid_return)
MessageTypeA * NON_NULL allocate() {


4. Why would I get a yellow circle on the signed overflow in a
statement as mundane as this? Have I misunderstood what the assertion
means, becuse it seems trivially true?

uint8_t const * in = data_in;
/*@ assert rte: signed_overflow: (int)*in<<8 ≤ 2147483647; */
uint16_t msgType = (*in++)<<8;


5. In my code, I can safely downcast a struct (as I do in
MessageTypeA_serialize and MessageTypeA_equals) because the superclass
has a field indicating what it can safely be downcast into. What
annotations should I use to express this?


6. As I understand it, function pointers are not currently supported.
For my initial use of function pointers (a lookup table, fixed at
compile time, from message type to serializer/deserializer) I can
probably use a switch statement instead, but I'm curious as to whether
support is on the roadmap?


Thanks very much!

Michael Tandy