--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2018 ---
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>