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



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>