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] Jessie plugin
- Subject: [Frama-c-discuss] Jessie plugin
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Mon, 07 May 2012 20:31:14 +0200
- In-reply-to: <4FA274EC.3040807@inria.fr>
- References: <CAEtoXR1wZO6+KMH4kGS-iUBr1PoDjQpY2rtXaU5uA+ARC2BKLQ@mail.gmail.com> <4FA274EC.3040807@inria.fr>
On 05/03/2012 02:07 PM, Claude Marche wrote: > The right question is: are AB_Ptr and CD_ptr separated ? My guess is > that if you pass the same pointer for both arguments, your contract > with behaviors does not hold. > > - Claude > Sorry for my initial short answer, it was only a quick guess og what could be the problem. Looking at the program in more details, I think the problem is more on your understanding of the \exact construct. What is misleading in your example is that the ensures clause is the same in both behaviors. Which makes the version without behaviors simpler to prove. In other words, I have the feeling that you think that your two assumes clauses exactly specify the two possible paths in the code, but this is wrong. This may be clearer on such a code : int result; /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr); @ behavior zero: @ assumes \exact(*AB_Ptr) > \exact(*CD_Ptr) ; @ ensures result == 1 @ behavior one: @ assumes \exact(*AB_Ptr) <= \exact(*CD_Ptr); @ ensures result == 0; @ */ void test(float *AB_Ptr, float *CD_Ptr) { if (*AB_ptr > *CD_ptr) result = 1; else result = 0; } Which should not be proved. But should be proved if you remove the \exact's So, Are you sure you understand the meaning of \exact ? - Claude
- Follow-Ups:
- [Frama-c-discuss] Jessie plugin
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Jessie plugin
- References:
- [Frama-c-discuss] Jessie plugin
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Jessie plugin
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Jessie plugin
- Prev by Date: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Next by Date: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Previous by thread: [Frama-c-discuss] Jessie plugin
- Next by thread: [Frama-c-discuss] Jessie plugin
- Index(es):