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