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

  • Subject: [Frama-c-discuss] Jessie : \initialized predicate
  • From: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Mon, 2 Jul 2018 17:33:37 +0200
  • In-reply-to: <CAJCNPir8BUDtSpvxJL0jw228Cxfp=ccZ2cQjMXDZexK7WRLqUQ@mail.gmail.com>
  • References: <CAJCNPir8BUDtSpvxJL0jw228Cxfp=ccZ2cQjMXDZexK7WRLqUQ@mail.gmail.com>
Hello,

The '\initialized' annotations to some parts of the Frama-C libc were 
added recently. Compatibility with Jessie was dropped recently in 
Frama-C as well, so the new Frama-C libc was not tested with Jessie.

Here are a few suggestions which might work:

1. Manually remove all annotations containing the \initialized predicate;

2. Use the libc from an older Frama-C version (e.g. copy the share/libc 
directory from an old Frama-C .tar.gz to overwrite the FRAMAC_SHARE/libc 
from a newer installation);

3. Modify Jessie or create a Frama-C plug-in to ignore/strip all 
annotations containing label "initialization" (which identifies labels 
using the \initialized predicate), but this requires the libc from 
Frama-C Chlorine (previously, such predicates were not named explicitly 
like that).

Solution 3 is the "ideal" one, in that it should allow Jessie to ignore 
only annotations which it does not understand, but it requires changing 
the code.

Solution 2 is hackish and prone to other issues (mixing different 
versions of Frama-C and its libc is not recommended), but quick to try.

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.


Overall, note that the Frama-C libc is simply a collection of annotated 
headers and sources, and the annotations are a best-effort based on 
POSIX, but they should not be treated as the absolute truth, and there 
is no hard-coded behavior related to it; feel free to read and edit them 
if that seems appropriate.



On 02/07/18 17:04, Elarif Mohamed wrote:
> Hi,
>
> I know this must have already been asked, but i can't find the thread.
>
> Here's my problem : I'm trying to process an annoted c source file, 
> dealing with real time functions, and the sys/time.h header.
> Jessie, when called, use frama-c's own annoted time.h header, which 
> contains a \initialized predicate, unsupported by Jessie.
>
> And then the translation from annoted C to .jc results with an error :
>
> -$ frama-c -cpp-extra-args="-DPOSIX -D_POSIX_SOURCE -D_GNU_SOURCE 
> -Wall -W" -jessie -jessie-gen-only my_time.c
>  FRAMAC_SHARE/libc/time.h:92:[jessie] failure: \initialized operator
>  [jessie] user error: Unsupported feature(s).
>      Jessie plugin can not be used on your code.
>
> 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> ) Maybe using older versions of Frama-C ?
>
> My Why/Why3/Frama-C suite tools works perfectly on other annoted 
> source files (without real time), but here's my versions :
>
> Why 2.40
> Why3 0.88.3
> Frama-C Sulfur-20171101
>
> Sorry if the answer is obvious, but i'm quite new to Frama-C and 
> Jessie, and would appreciate any help !
>
> Best regards,
>
> Elarif MOHAMED.
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/LIST
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180702/a8e0f7f1/attachment-0001.html>
-------------- 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/20180702/a8e0f7f1/attachment-0001.bin>