--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on November 2016 ---
Hello, Just to complete Virgile's answer: your specifications have some `\valid` where they should have `\valid_read`. `\valid` implies that the memory location is writable, so it cannot be const (as in your code). Replacing them allows the value analysis to proceed. On 22/11/2016 09:38, Michael Tandy wrote: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Ingénieur-chercheur CEA/LIST Laboratoire Sûreté et Sécurité des Logiciels -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161122/e5d7a9d5/attachment-0001.bin>