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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Tue, 22 Nov 2016 10:23:52 +0100
  • In-reply-to: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
  • References: <CAHGSkqjVKhG8Y74QkiL1WGsqgPXo_JjJHOgNkvu=iY7LD-DrpA@mail.gmail.com>
Hello,

2016-11-22 9:38 GMT+01:00 Michael Tandy <framacdisc at mjt.me.uk>:

> 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 :)

This is documented in the Frama-C user manual, available, together
with ACSL manual and many plug-ins specific manuals, at
http://frama-c.com/support.html.
More specifically, red-orange indicates invalid-under-hyp, i.e. a
property that is false, but under assumptions (other ACSL annotations)
that have not yet been proved. There's no green-red, I assume you mean
green-orange, which is valid-under-hyp, indicating that the property
is true under unproved assumptions. Blue circle indicates a property
for which no verification attempt has been done. Yellow means unknown:
(at least) one plug-in tried to verify the property, but couldn't
decide in one sense or the other. And as you guessed green means valid
(with all assumptions validated). Regarding assumptions, note that not
all plug-ins bother to explicit the dependencies of an ACSL property
for which they emit a status (in particular Value does not, as it
would be very impractical to either flag all the ACSL annotations
encountered since the start of the main entry point as dependencies of
the current property or to maintain a fine-grained account of which
property contributed to restrict which part of the abstract state so
as to make the current one valid), so that a green bullet does not
always means that everything is alright as long as some yellow ones
are left.

> 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>

It means that the current abstract state is bottom, i.e. that the
abstract execution never reaches the corresponding point in the
program. It can indicate a dead branch that is not exercised by the
entry point, or that a true alarm occurs before reaching that point.

> 3. How does one assert that a method returns a valid pointer? I've
> tried the following guesses without success:

Using the ensures clauses presented in the ACSL manual:

/*@ ensures \valid(\result); */

>
> 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;

Well, this statement is not as trivial as it seems. In particular it
mixes a bitwise operation with an arithmetic operator, which can be
very complicated for provers. In any case, it is impossible to tell
why "a yellow circle" occurs if you don't indicate exactly the frama-c
command that led to this result (and if this was obtained with WP, the
most probable answer will be "because provers are not powerful
enough").

>
>
> 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?

I'm afraid that WP will have trouble understand that, but a possible
way would be something like

\forall Message* a; \valid(a) && a->messageType == MESSAGE_TYPE_A ==>
\valid((MessageTypeA*)a);

> 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?
>

Function pointers are supported in the kernel and Value analysis. WP
has an experimental and mostly undocumented support for them.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile