--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie : \initialized predicate



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>