--- layout: fc_discuss_archives title: Message 12 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



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