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 : \initialized predicate

At the risk of sounding un-enthusiastic, I do not consider not using the
libc packaged with Frama-C a viable solution. The Frama-C team has spent
countless hours specifying useful functions from the libc using
(1) exact preconditions [1]
(2) reasonably precise postconditions
(3) flow informations, even in presence of tricky aliasing
(4) taking into acount things such as non-determinism, or internal states
(e.g. the filesystem)
>From our experience, getting those specifications right is incredibly
tricky in quite a few cases.

At the very least, I would suggest using Andre's first solution, i.e.
remove the offending \initialized predicate from the preconditions and
postconditions of our libc. And the right long-term solution here is to
patch Jessie, or to use the WP plugin from Frama-C [2].

HTH,

[1] in the sense that we capture only the requirements from ISO-C/Posix.
[2] which does understand \initialized either, but at least VCs can be
generated because \initialized is translated as \true or \false according
to the polarity of the predicate.


On Wed, Jul 4, 2018 at 5:04 PM Claude Marché <Claude.Marche at inria.fr> wrote:

>
>
> Le 02/07/2018 à 17:33, Andre Maroneze a écrit :
> > 1. Manually remove all annotations containing the \initialized predicate;
> > Solution 1 is a short-term solution that should not have negative
> > side-effects, except for plug-ins such as Eva, which use these
> annotations.
>
> Yes, or simply do not use the header file proposed by Frama-C and write
> your own version, so that you can think carefully about what
> requirement/specifications you want to rely on concerning functions in
> time.h
>
> >> I know, the message is quite explicit, but isn't there really any way
> >> to use Jessie with a real time program ? ( using the #include
> >> <sys/time.h> )
>
> Yes you can! same answer: it is only a matter of understanding the
> requirements/specifications you want to rely on about time functions.
> "only a matter of ... " but it is probably the most important question
> you should ask yourself first: what do you want to prove on your code?
>
> Hope this helps,
>
> - Claude
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss



-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180704/e115f726/attachment.html>