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: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Tue, 22 Nov 2016 10:35:36 +0100
  • In-reply-to: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
  • References: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
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>