Frama-C-discuss mailing list archives

Maria.Christofi at gemalto.com (Christofi Maria) · Sat, 18 Jun 2011 18:39:12 +0200

Hello again!

Thank you for your answer :)
It seems that it is exactly what I want to do, but I have not succeded. 

Actually, when I am typing frama-c -jessie-why-opt="-fast-wp" test.c (if we suppose that the file was test.c), it is running gcc and that's all. 

So in my window, it appears preprocessing with "gcc -C -E -I test.c" and it finishes there. Is that normal? Am I doing something wrong?

Maria

-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of frama-c-discuss-request at lists.gforge.inria.fr
Sent: samedi 18 juin 2011 12:01
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Frama-c-discuss Digest, Vol 37, Issue 11

Send Frama-c-discuss mailing list submissions to
	frama-c-discuss at lists.gforge.inria.fr

To subscribe or unsubscribe via the World Wide Web, visit
	http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
or, via email, send a message with subject or body 'help' to
	frama-c-discuss-request at lists.gforge.inria.fr

You can reach the person managing the list at
	frama-c-discuss-owner at lists.gforge.inria.fr

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Frama-c-discuss digest..."

Today's Topics:

   1. multiple switch on one variable (Christofi Maria)
   2. Re: multiple switch on one variable (Pascal Cuoq)
   3. Re: multiple switch on one variable (Pascal Cuoq)

----------------------------------------------------------------------

Message: 1
Date: Fri, 17 Jun 2011 12:43:34 +0200
From: Christofi Maria <Maria.Christofi at gemalto.com>
Subject: [Frama-c-discuss] multiple switch on one variable
To: "frama-c-discuss at lists.gforge.inria.fr"
	<frama-c-discuss at lists.gforge.inria.fr>
Message-ID:
	<E6A62071A6ED164AB84A12397A76F95704193DFFC4EB at ABSEXCFWP02.gemalto.com>
Content-Type: text/plain; charset="us-ascii"

Hello,

I need some help..
Actually, if we have two "switch"  on the same variable, frama-c doesn't seem to understand that it is really the same variable.
Let me explain what I mean:

Suppose that you have the following code:

/*@ ensures \result == x || \result == a + b; */

int main (int a, int b, int x)
{ int y;
                switch (x)
                {
                case 1 :  a = 5;  break;
case 2:  b = 3 ; break;
}

y = a + b;

switch   (x)
{
case 3: b= 1; break;
case 4: a = 0; break;
}

if (a =5) return x;
return y;
}

Remark that x is not modified during the function.

In that case, frama-c/ Jessie will check the postcondition for the cases that (x=1 and x=3) as well as (x=1 and x=4) and go on..
Unless that normally we will never have both x= 1 and x= 3 at the same time.

Does anyone have any idea about how to explain that to frama-c?

Thanks in advance!
Maria

PS: I am using Beryllium-20090902. So if it is not the cas for a later version, please let me know.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110617/e694300c/attachment.html>

------------------------------

Message: 2
Date: Fri, 17 Jun 2011 12:59:25 +0200
From: Pascal Cuoq <pascal.cuoq at gmail.com>
Subject: Re: [Frama-c-discuss] multiple switch on one variable
To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Message-ID: <BANLkTimtiMyhd1FbhGfMjUGqp4DYN02RQg at mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1

Hello,

your example brings up several remarks.

> /*@ ensures \result == x || \result == a + b; */
>
> int main (int a, int b, int x)

1/ You are writing a post-condition involving arguments
that are modified inside the function as if they were
local variables. The occurrences of a and b in the
post-condition refer to the initial values of a and b, not
the values at the end of the function. Are you sure
you want to do this? I am sure I will get confused before
the end of this discussion.

2/ In Frama-C Carbon with alt-ergo 0.92.1, the post-condition
goals for your function are all proved. There are some arithmetic
overflow warnings, but considering that you do not give the
provers hypotheses on the values of variables that could prevent
overflows, I would tend to think it is right without looking.

3/ It is principally about the value analysis and in fact,
option -jessie may even automatically imply -simplify-cfg
(I do not know how it works), but you may be interested in
this blog post:

http://blog.frama-c.com/index.php?post/2011/02/28/switch-statements-in-the-value-analysis

Pascal

------------------------------

Message: 3
Date: Fri, 17 Jun 2011 13:13:47 +0200
From: Pascal Cuoq <pascal.cuoq at gmail.com>
Subject: Re: [Frama-c-discuss] multiple switch on one variable
To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Message-ID: <BANLkTims_LTBXB+JeOBrd7oqQSr7fvwWNw at mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1

> In that case, frama-c/ Jessie will check the postcondition for the cases
> that (x=1 and x=3) as well as (x=1 and x=4) and go on..
>
> Unless that normally we will never have both x= 1 and x= 3 at the same time.

Oh, I think I understand your question now.

You are looking at the various goals generated for the single
post-condition and you
see things such as:

integer_of_int32(x_0) = 3

and:

integer_of_int32(x_0) = 5

as hypotheses for the same goal,
and you are wondering why Why considers this impossible case.

This is normal. It has not started to think yet at the time it has
generated these two incompatible hypotheses. Don't worry, automated
theorem provers are very good at noticing that there is \false in the
hypotheses and concluding directly (here, reproducing the reasoning
that whatever logical property needs to be verified is true because
the case where x is both 3 and 5 simultaneously never happens).

If you are worried that with all these impossible cases, the total
number of goals will be too large, use option
-jessie-why-opt="-fast-wp". This will generate a single goal, which
will of course be more complex.

Pascal

------------------------------

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

End of Frama-c-discuss Digest, Vol 37, Issue 11
***********************************************

Frama-C-discuss mailing list archives

[Frama-c-discuss] Frama-c-discuss Digest, Vol 37, Issue 11