--- layout: fc_discuss_archives title: Message 1 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



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